Type checking with universes

DOI10.1016/0304-3975(90)90108-TzbMath0737.68013OpenAlexW2014836228MaRDI QIDQ1177937

Robert Harper, Robert Pollack

Publication date: 26 June 1992

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(90)90108-t

zbMATH Keywords

calculus of constructionsuniversestype checkingwell-typedness

Mathematics Subject Classification ID

Theory of programming languages (68N15) General topics in the theory of software (68N01)

Related Items

Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism ⋮ Categorical abstract machines for higher-order typed \(\lambda\)-calculi ⋮ Program specification and data refinement in type theory ⋮ Finitary type theories with and without contexts ⋮ Checking algorithms for Pure Type Systems ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ Formal polytypic programs and proofs ⋮ Algebra of programming in Agda: Dependent types for relational program derivation ⋮ Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I

Uses Software

• ML
• Nuprl
• Automath
• LEGO

Cites Work

• Semantics of data types. International Symposium, Sophia-Antipolis, France, June 27-29, 1984. Proceedings
• Pebble, a kernel language for modules and abstract data types
• The lambda calculus, its syntax and semantics
• A theory of type polymorphism in programming
• A higher-order calculus and theory abstraction
• Constructive mathematics and computer programming
• The Type Theory of PL/CV3
• A framework for defining logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item