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

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) 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)

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

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)