scientific article; zbMATH DE number 5173450

MaRDI QIDQ3593498zbMATH OpenFDO

Authors Andreas Abel, Thierry Coquand

Publication date 20 July 2007

zbMATH Keywords

bidirectional type checking algorithm

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Untyped algorithmic equality for Martin-Löf's logical framework with surjective pairs
• Martin's axiom, omitting types, and complete representations in algebraic logic
• Well-ordering proofs for Martin-Löf type theory
• scientific article; zbMATH DE number 4137744
• Exploiting positive equality in a logic of equality with uninterpreted functions
• On irrelevance and algorithmic equality in predicative type theory
• Algorithmic correspondence and canonicity for non-distributive logics
• scientific article; zbMATH DE number 3970817
• Polynomial-time Martin-Löf type theory
• scientific article; zbMATH DE number 554983

Cited in

(4)

• Equality checking for general type theories in Andromeda 2
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• Explicit substitutions for contextual type theory
• What does it take to certify a conversion checker?

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 Q3593498)