scientific article; zbMATH DE number 2079018
From MaRDI portal
Publication:4474830
Recommendations
- The \(\lambda \)-calculus and the unity of structural proof theory
- scientific article; zbMATH DE number 1980937
- 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
(51)- 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
- The \(\lambda \)-calculus and the unity of structural proof theory
- Resource operators for \(\lambda\)-calculus
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4474830)
