A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure
- 1 January 1995
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- A typed pattern calculusPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- λν, a calculus of explicit substitutions which preserves strong normalisationJournal of Functional Programming, 1996
- Constructive logics Part I: A tutorial on proof systems and typed λ-calculiTheoretical Computer Science, 1993
- On the unity of logicAnnals of Pure and Applied Logic, 1993
- A new constructive logic: classic logicMathematical Structures in Computer Science, 1991
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- Normalization as a homomorphic image of cut-eliminationAnnals of Mathematical Logic, 1977
- The correspondence between cut-elimination and normalizationAnnals of Mathematical Logic, 1974