Synthesis of ML programs in the system Coq

DOI10.1016/S0747-7171(06)80007-6zbMath0804.68132OpenAlexW2135625856MaRDI QIDQ1322847

Benjamin Werner, Christine Paulin-Mohring

Publication date: 12 January 1995

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0747-7171(06)80007-6

zbMATH Keywords

optimizationcalculus of constructionsterminationprogram synthesisMLCoqprimitive recursive functionalsfixpointfunctional programproof development

Mathematics Subject Classification ID

Related Items (8)

Code-carrying theories ⋮ Recent advances in program verification through computer algebra ⋮ Logic of refinement types ⋮ Developing certified programs in the system Coq the program tactic ⋮ A Short Presentation of Coq ⋮ Uniform Heyting arithmetic ⋮ Tool Support for Proof Engineering ⋮ Program extraction from normalization proofs

Uses Software

• Coq
• ML
• Nuprl
• LCF

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

This page was built for publication: Synthesis of ML programs in the system Coq