Equivalences between logics and their representing type theories

DOI10.1017/S0960129500000785zbMath0868.03003MaRDI QIDQ4862761

Philippa Gardner

Publication date: 12 February 1996

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

natural representationentailment relationadequate representationlogical framework LF\(^ +\)long beta-eta normal formmultiple universes

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items (1)

Formalizing adequacy: a case study for higher-order abstract syntax

Uses Software

• HOL
• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• Linear logic
• Using typed lambda calculus to implement formal systems on a machine
• Simple consequence relations
• The foundation of a generic theorem prover
• Fibered categories and the foundations of naive category theory
• A framework for defining logics
• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
• A formulation of the simple theory of types

This page was built for publication: Equivalences between logics and their representing type theories