scientific article; zbMATH DE number 1927413

MaRDI QIDQ4484330zbMATH OpenFDO

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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

Cited in

(15)

• Efficient execution in an automated reasoning environment
• 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
• Mechanically certifying formula-based Noetherian induction reasoning
• Handcrafted inversions made operational on operational semantics

Describes a project that uses

Uses Software

• LEGO
• Jakarta
• Coq

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)