A higher-order calculus and theory abstraction

DOI10.1016/0890-5401(91)90062-7zbMath0719.03004OpenAlexW2059944616MaRDI QIDQ2639838

Zhaohui Luo

Publication date: 1991

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(91)90062-7

zbMATH Keywords

program specificationhigher-order logicstrong normalizationrealizability modelExtended Calculus of Constructionsabstract theoryAbstract reasoningextension of Martin-Löf's type theoryinteractive proof developmentproof-theoretic propertiestheory of dependent types

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Second- and higher-order arithmetic and fragments (03F35)

Related Items

Program specification and data refinement in type theory ⋮ Constructive sets in computable sets ⋮ An intuitionistic set-theoretical model of fully dependent CC ⋮ Type checking with universes ⋮ The extended calculus of constructions (ECC) with inductive types ⋮ A simple model construction for the Calculus of Constructions ⋮ Semantics of constructions. I: The traditional approach ⋮ Manifest Fields and Module Mechanisms in Intensional Type Theory

Uses Software

• Nuprl
• Automath
• LEGO
• Cambridge LCF

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The system \({\mathcal F}\) of variable types, fifteen years later
• Generalized algebraic theories and contextual categories
• Pebble, a kernel language for modules and abstract data types
• The calculus of constructions
• A small complete category
• Fundamentals of contemporary set theory
• On functors expressible in the polymorphic typed lambda calculus
• Domain theoretic models of polymorphism
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Locally cartesian closed categories and type theory
• Godel's interpretation of intuitionism
• Logic and Computation
• A framework for defining logics
• The Universe of Set Theory