Program calculation in Coq

DOI10.1007/978-3-642-17796-5_10MaRDI QIDQ3067474zbMATH OpenOpenAlexFDO

Authors Julien Tesson, Zhenjiang Hu, Masato Takeichi, Hideki Hashimoto, F. Loulergue

Publication date 21 January 2011

Published in Algebraic Methodology and Software Technology (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-17796-5_10

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Synthesis of ML programs in the system Coq
• An introduction to programming and proving with dependent types in Coq
• Verifying programs in the calculus of inductive constructions
• From proposition to program. Embedding the refinement calculus in Coq
• Axiomatisations, proofs, and formal specifications of algorithms: Commented case studies in the coq proof assistant

Cites work

• A Declarative Language for the Coq Proof Assistant
• A survey of strategies in rule-based program transformation systems
• Advanced Functional Programming
• Algebra of programming in Agda: Dependent types for relational program derivation
• Categories, relations and dynamic programming
• Cayenne -- a language with dependent types
• Dependently typed programming in Agda
• First-Class Type Classes
• Higher order matching for program transformation
• scientific article; zbMATH DE number 910715 (Why is no real title available?)
• The derivation of systolic computations

Cited in

(5)

• Calculating certified compilers for non-deterministic languages
• Constructive Galois connections
• Calculations
• Recursion schemes in Coq
• Program optimisations via hylomorphisms for extraction of executable code

Describes a project that uses

Uses Software

• Agda
• AoPA
• Coq
• Cayenne
• Epigram

This page was built for publication: Program calculation in Coq

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