Types for Proofs and Programs

DOI10.1007/11617990MaRDI QIDQ5897607zbMATH OpenOpenAlexFDO

Authors Conor McBride, Healfdene Goguen, James McKinna

Publication date 13 November 2006

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

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65)

Recommendations

• scientific article; zbMATH DE number 1405632
• On lists and other abstract data types in the calculus of constructions
• scientific article; zbMATH DE number 4014064
• Inductive families
• scientific article; zbMATH DE number 1841846

Cited in

(8)

• Eliminating dependent pattern matching without K
• scientific article; zbMATH DE number 7649978 (Why is no real title available?)
• Congruence closure in intensional type theory
• Types for Proofs and Programs
• The gentle art of levitation
• Types for Proofs and Programs
• scientific article; zbMATH DE number 431766 (Why is no real title available?)
• On the Implementation of Construction Functions for Non-free Concrete Data Types

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5897607)