scientific article; zbMATH DE number 2185663

MaRDI QIDQ3024837zbMATH OpenFDO

Authors Martin Hofmann

Publication date 4 July 2005

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2003152
• Type theory in type theory using quotient inductive types
• scientific article; zbMATH DE number 1841843
• Quotients over Minimal Type Theory
• Quotients, inductive types, and quotient inductive types

Cited in

(9)

• Equilogical spaces
• A language with type-dependent equality
• scientific article; zbMATH DE number 1841843 (Why is no real title available?)
• Quotients by idempotent functions in Cedille
• Quotients over Minimal Type Theory
• scientific article; zbMATH DE number 7649955 (Why is no real title available?)
• Elimination of extensionality in Martin-Löf type theory
• Coalgebras in functional programming and type theory
• Synthetic 1-categories in directed type theory

This page was built for publication:

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