Program development in constructive type theory

DOI10.1016/0304-3975(92)90037-GzbMath0760.68012MaRDI QIDQ1190474

Didier Galmiche

Publication date: 26 September 1992

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

program derivation from proofsprogramming with proofs

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Related Items (2)

On proof normalization in linear logic ⋮ Proof-search in type-theoretic languages: An introduction

Uses Software

• Nuprl
• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The system \({\mathcal F}\) of variable types, fifteen years later
• Constructing recursion operators in intuitionistic type theory
• The calculus of constructions
• Terminating general recursion
• A synthesis of several sorting algorithms
• The foundation of a generic theorem prover
• Constructive mathematics and computer programming
• A set constructor for inductive sets in Martin-Löf's type theory

This page was built for publication: Program development in constructive type theory