The Implicit Calculus of Constructions as a Programming Language with Dependent Types

DOI10.1007/978-3-540-78499-9_26zbMath1138.68356OpenAlexW1554068457MaRDI QIDQ5458373

Bruno Bernardo, Bruno Barras

Publication date: 11 April 2008

Published in: Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-78499-9_26

Mathematics Subject Classification ID

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

Related Items (5)

Linear Dependent Type Theory for Quantum Programming Languages ⋮ Extracting functional programs from Coq, in Coq ⋮ A dependent dependency calculus ⋮ Unnamed Item ⋮ Is Impredicativity Implicitly Implicit

Uses Software

• Coq
• Nuprl

Cites Work

• Unnamed Item
• Combining programming with theorem proving
• A Brief Overview of PVS
• Subset Coercions in Coq
• On the Strength of Proof-Irrelevant Type Theories
• The view from the left
• Introduction to generalized type systems
• Types for Proofs and Programs

This page was built for publication: The Implicit Calculus of Constructions as a Programming Language with Dependent Types