An algorithm for type-checking dependent types

DOI10.1016/0167-6423(95)00021-6zbMath0853.68102OpenAlexW2090046646MaRDI QIDQ1916364

Thierry Coquand

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

zbMATH Keywords

type-checker

Mathematics Subject Classification ID

Parallel algorithms in computer science (68W10)

Related Items

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

• LCF