Synthesis of ML programs in the system Coq
From MaRDI portal
Publication:1322847
DOI10.1016/S0747-7171(06)80007-6zbMath0804.68132MaRDI QIDQ1322847
Christine Paulin-Mohring, Benjamin Werner
Publication date: 12 January 1995
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
optimization; calculus of constructions; termination; program synthesis; ML; Coq; primitive recursive functionals; fixpoint; functional program; proof development
68N15: Theory of programming languages
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Program extraction from normalization proofs, Uniform Heyting arithmetic, Code-carrying theories, A Short Presentation of Coq
Uses Software
Cites Work
- Comparing integrated and external logics of functional programs
- Proving termination of normalization functions for conditional expressions
- Terminating general recursion
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Edinburgh LCF. A mechanized logic of computation
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item