Program Calculation in Coq

DOI10.1007/978-3-642-17796-5_10zbMath1308.68049OpenAlexW1605536043MaRDI QIDQ3067474

Julien Tesson, Masato Takeichi, Zhenjiang Hu, Frédéric Loulergue, Hideki Hashimoto

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)

Related Items (2)

Calculating Certified Compilers for Non-deterministic Languages ⋮ Constructive Galois Connections

Uses Software

• Coq
• Cayenne
• Epigram
• Agda
• AoPA

Cites Work

• Unnamed Item
• Unnamed Item
• The derivation of systolic computations
• A survey of strategies in rule-based program transformation systems
• A Declarative Language for the Coq Proof Assistant
• First-Class Type Classes
• Algebra of programming in Agda: Dependent types for relational program derivation
• Dependently Typed Programming in Agda
• Categories, relations and dynamic programming
• Cayenne—a language with dependent types
• Advanced Functional Programming

This page was built for publication: Program Calculation in Coq