A Gentzen-style sequent calculus of constructions with expansion rules

DOI10.1016/S0304-3975(98)00195-9zbMath0945.03082MaRDI QIDQ1575638

Jonathan P. Seldin

Publication date: 21 August 2000

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

zbMATH Keywords

calculus of constructionsnatural deductiontyped lambda-calculusGentzen-style L-formulation

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items (4)

An epistemic logic for becoming informed ⋮ Interpreting HOL in the calculus of constructions ⋮ Variants of the basic calculus of constructions ⋮ Type Theories from Barendregt’s Cube for Theorem Provers

Cites Work

• Combinatory logic. With two sections by William Craig.
• Coquand's calculus of constructions: A mathematical foundation for a proof development system
• On the proof theory of Coquand's calculus of constructions
• Unnamed Item
• Unnamed Item

This page was built for publication: A Gentzen-style sequent calculus of constructions with expansion rules