A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation

DOI10.1007/978-3-642-38946-7_12zbMath1273.03106OpenAlexW2184421553MaRDI QIDQ5300899

Miguel Pagano, Daniel Fridlender

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

Martin-Löf's type theorysubtypingintuitionistic type theorytype checkingnormalisation by evaluation

Mathematics Subject Classification ID

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

Related Items (1)

Pure type systems with explicit substitutions

This page was built for publication: A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation