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

DOI10.1007/978-3-642-38946-7_12zbMATH Open1273.03106OpenAlexW2184421553MaRDI QIDQ5300899FDOQ5300899

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

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

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)

Cited In (4)

• Title not available (Why is that?)
• 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)