Algebraic proofs of cut elimination

DOI10.1016/S1567-8326(01)00009-1zbMath1015.68174OpenAlexW2093985783WikidataQ127087656 ScholiaQ127087656MaRDI QIDQ1349247

Jeremy Avigad

Publication date: 21 May 2002

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s1567-8326(01)00009-1

zbMATH Keywords

algebraic proofscut-elimination theorems

Mathematics Subject Classification ID

Related Items (4)

An ecumenical notion of entailment ⋮ Kripke models for classical logic ⋮ Forcing in Proof Theory ⋮ Saturated models of universal theories

Cites Work

• Two applications of Boolean models
• Constructivism in mathematics. An introduction. Volume I
• Sheaves in geometry and logic: a first introduction to topos theory
• Transfer principles in nonstandard intuitionistic arithmetic
• Saturated models of universal theories
• Proof theory in the USSR 1925–1969
• The correspondence between cut-elimination and normalization
• Ein Ausgezeichnetes Modell Für Die Intuitionistische Typenlogik
• Constructive Sheaf Semantics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Algebraic proofs of cut elimination