A higher-order calculus and theory abstraction
From MaRDI portal
Publication:2639838
DOI10.1016/0890-5401(91)90062-7zbMath0719.03004OpenAlexW2059944616MaRDI QIDQ2639838
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
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
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
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