Synthesis of ML programs in the system Coq
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 2003158
- Verifying programs in the calculus of inductive constructions
- scientific article; zbMATH DE number 1070623
- Proofs and programs: A naïve approach to program extraction
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
Cites work
- scientific article; zbMATH DE number 4019061 (Why is no real title available?)
- scientific article; zbMATH DE number 4147469 (Why is no real title available?)
- scientific article; zbMATH DE number 4164171 (Why is no real title available?)
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 3928956 (Why is no real title available?)
- scientific article; zbMATH DE number 3688777 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 46869 (Why is no real title available?)
- scientific article; zbMATH DE number 47007 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 512790 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Comparing integrated and external logics of functional programs
- Edinburgh LCF. A mechanized logic of computation
- Proving termination of normalization functions for conditional expressions
- Terminating general recursion
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
Cited in
(28)- Tool support for proof engineering
- The Scallina grammar. Towards a Scala extraction for Coq
- scientific article; zbMATH DE number 517012 (Why is no real title available?)
- PML2: integrated program verification in ML
- Types for Proofs and Programs
- scientific article; zbMATH DE number 6528605 (Why is no real title available?)
- Typing total recursive functions in Coq
- scientific article; zbMATH DE number 2003158 (Why is no real title available?)
- Theoretical computer science: computability, decidability and logic
- Extracting functional programs from Coq, in Coq
- Uniform Heyting arithmetic
- Developing certified programs in the system Coq the program tactic
- Recent advances in program verification through computer algebra
- ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti
- scientific article; zbMATH DE number 1927413 (Why is no real title available?)
- Program extraction from normalization proofs
- Recursion schemes in Coq
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- scientific article; zbMATH DE number 2061716 (Why is no real title available?)
- Program calculation in Coq
- Synthesis of distributed mobile programs using monadic types in Coq
- A proof system for MSVL programs in Coq
- Code-carrying theories
- Implementing hash-consed structures in Coq
- Producing certified functional code from inductive specifications
- Logic of refinement types
- A Short Presentation of Coq
- scientific article; zbMATH DE number 1670740 (Why is no real title available?)
This page was built for publication: Synthesis of ML programs in the system Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1322847)
