An algorithm for type-checking dependent types
From MaRDI portal
Publication:1916364
DOI10.1016/0167-6423(95)00021-6zbMath0853.68102OpenAlexW2090046646MaRDI QIDQ1916364
Publication date: 3 July 1996
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0167-6423(95)00021-6
Related Items (11)
Indexed types ⋮ Realist Consequence, Epistemic Inference, Computational Correctness ⋮ Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda ⋮ Unnamed Item ⋮ A Partial Type Checking Algorithm for Type:Type ⋮ Termination checking with types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance ⋮ Typed Applicative Structures and Normalization by Evaluation for System F ω ⋮ Unnamed Item
Uses Software
This page was built for publication: An algorithm for type-checking dependent types