scientific article; zbMATH DE number 5173450

zbMATH Open1121.68026MaRDI QIDQ3593498FDOQ3593498

Authors: Andreas Abel, Thierry Coquand 

Publication date: 20 July 2007

Title of this publication is not available (Why is that?)

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

zbMATH Keywords

bidirectional type checking algorithm

Mathematics Subject Classification ID

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

Cited In (2)

• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• Equality checking for general type theories in Andromeda 2

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)