Types for Proofs and Programs

DOI10.1007/B98246zbMath1100.68546OpenAlexW4298423642MaRDI QIDQ5712325

Conor McBride, Edwin Brady, James McKinna

Publication date: 23 December 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b98246

Mathematics Subject Classification ID

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

Related Items (7)

Foundations of dependent interoperability ⋮ Turing-Completeness Totally Free ⋮ Extracting functional programs from Coq, in Coq ⋮ Elaborating dependent (co)pattern matching: No pattern left behind ⋮ Graded modal dependent type theory ⋮ Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic ⋮ The Implicit Calculus of Constructions as a Programming Language with Dependent Types

Uses Software

• Plastic
• LEGO

This page was built for publication: Types for Proofs and Programs