scientific article; zbMATH DE number 1927413

zbMATH Open1013.68539MaRDI QIDQ4484330FDOQ4484330

Authors: Gilles Barthe, Pierre Courtieu 

Publication date: 12 June 2003

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2410/24100031.htm

Title of this publication is not available (Why is that?)

Recommendations

• Synthesis of ML programs in the system Coq
• Producing certified functional code from inductive specifications
• scientific article; zbMATH DE number 1070623
• Efficient execution in an automated reasoning environment
• scientific article; zbMATH DE number 1692947

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (15)

• A certified reduction strategy for homological image processing
• Using Structural Recursion for Corecursion
• The world's shortest correct exact real arithmetic program?
• CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
• Tool-assisted specification and verification of typed low-level languages
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
• Analysing and Compiling Coroutines with Abstract Conjunctive Partial Deduction
• LF+ in Coq for "fast and loose" reasoning
• Deciding Kleene algebra terms equivalence in Coq
• Deciding regular expressions (in-)equivalence in Coq
• Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves
• Handcrafted inversions made operational on operational semantics
• Mechanically certifying formula-based Noetherian induction reasoning
• Efficient execution in an automated reasoning environment

Uses Software

• Coq
• Jakarta
• LEGO

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4484330)