Program calculation in Coq

DOI10.1007/978-3-642-17796-5_10zbMATH Open1308.68049OpenAlexW1605536043MaRDI QIDQ3067474FDOQ3067474

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

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
• scientific article; zbMATH DE number 1070623

Mathematics Subject Classification ID

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

Cites Work

• Dependently typed programming in Agda
• A Declarative Language for the Coq Proof Assistant
• A survey of strategies in rule-based program transformation systems
• The derivation of systolic computations
• Cayenne -- a language with dependent types
• Categories, relations and dynamic programming
• Title not available (Why is that?)
• Title not available (Why is that?)
• First-Class Type Classes
• Algebra of programming in Agda: Dependent types for relational program derivation
• Advanced Functional Programming

Cited In (4)

• Constructive Galois connections
• Calculating certified compilers for non-deterministic languages
• Calculations
• Recursion schemes in Coq

Uses Software

• Coq
• Cayenne
• Epigram
• Agda
• AoPA

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)