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

• Typed Lambda Calculi and Applications
• 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
• scientific article; zbMATH DE number 2102727
• 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

(3)

• 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

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)