A -caclulus structure isomorphic to Gentzen-style sequent calculus structure

Recommendations

The \(\lambda \)-calculus and the unity of structural proof theory
An isomorphism between a fragment of sequent calculus and an extension of natural deduction
The structural \(\lambda \)-calculus
Lambda terms for natural deduction, sequent calculus and cut elimination
A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language

Cited in

(52)

Representing scope in intuitionistic deductions
Permutability of proofs in intuitionistic sequent calculi
Termination of permutative conversions in intuitionistic Gentzen calculi
On the linear decoration of intuitionistic derivations
On the intuitionistic force of classical search
Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
Multi-focused proofs with different polarity assignments
Varieties of linear calculi
Pattern matching as cut elimination
Some general results about proof normalization
What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics
From axioms to synthetic inference rules via focusing
A coinductive approach to proof search through typed lambda-calculi
Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment
A unified procedure for provability and counter-model generation in minimal implicational logic
Call-by-name reduction and cut-elimination in classical logic
Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications
On the computational representation of classical logical connectives
Proofs, upside down. A functional correspondence between natural deduction and the sequent calculus
Structural focalization
A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language
Intersection types for the resource control lambda calculi
Characterising Strongly Normalising Intuitionistic Sequent Terms
The Logic of Proofs as a Foundation for Certifying Mobile Computation
Completing Herbelin’s Programme
Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
Justification logic as a foundation for certifying mobile computation
Three faces of natural deduction
Two loop detection mechanisms: a comparison
Term sequent logic
Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
Yet another bijection between sequent calculus and natural deduction
Strong Normalisation of Cut-Elimination That Simulates β-Reduction
A typed context calculus
Focused linear logic and the \(\lambda\)-calculus
Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
A strong bisimulation for a classical term calculus
Focusing Gentzen's LK proof system
Partial proof terms in the study of idealized proof search
Data layout from a type-theoretic perspective
Semi-axiomatic sequent calculus
Permutability in proof terms for intuitionistic sequent calculus with cuts
IMELL cut elimination with linear overhead
Proof search in classical propositional logic with partial proof terms
Separability and harmony in ecumenical systems
Sequent calculus and equational programming
Gentzen-Mints-Zucker duality
Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic
Two applications of logic programming to Coq
Linear logic using negative connectives
The \(\lambda \)-calculus and the unity of structural proof theory
Resource operators for \(\lambda\)-calculus

This page was built for publication: A \(\lambda\)-caclulus structure isomorphic to Gentzen-style sequent calculus structure

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4474830)