A type-checking algorithm for Martin-Löf type theory with subtyping based on normalisation by evaluation

DOI10.1007/978-3-642-38946-7_12MaRDI QIDQ5300899zbMATH OpenOpenAlexFDO

Authors Daniel Fridlender, Miguel Pagano

Publication date 28 June 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-38946-7_12

zbMATH Keywords

subtypingintuitionistic type theorytype checkingnormalisation by evaluationMartin-Löf's type theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Intuitionistic mathematics (03F55)

Recommendations

• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• Type checking dependent (record) types and subtyping
• scientific article; zbMATH DE number 1361477
• The simple type theory of normalisation by evaluation
• Subtyping dependent types

Cited in

(4)

• scientific article; zbMATH DE number 4052993 (Why is no real title available?)
• Pure type systems with explicit substitutions
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory

This page was built for publication: A type-checking algorithm for Martin-Löf type theory with subtyping based on normalisation by evaluation

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