scientific article; zbMATH DE number 2079018
From MaRDI portal
zbMath1044.03509MaRDI QIDQ4474830
Publication date: 21 July 2004
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
From axioms to synthetic inference rules via focusing, Pattern matching as cut elimination, On the linear decoration of intuitionistic derivations, A unified procedure for provability and counter-model generation in minimal implicational logic, Resource operators for \(\lambda\)-calculus, Proofs, Upside Down, Structural Focalization, Some general results about proof normalization, Characterising Strongly Normalising Intuitionistic Sequent Terms, Justification logic as a foundation for certifying mobile computation, Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications, Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\), Three faces of natural deduction, Two loop detection mechanisms: A comparison, Focused linear logic and the \(\lambda\)-calculus, Goal-oriented proof-search in natural deduction for intuitionistic propositional logic, A coinductive approach to proof search through typed lambda-calculi, Multi-focused proofs with different polarity assignments, Yet another bijection between sequent calculus and natural deduction, Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment, Call-by-name reduction and cut-elimination in classical logic, The Logic of Proofs as a Foundation for Certifying Mobile Computation, A typed context calculus, What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics, The \(\lambda \)-calculus and the unity of structural proof theory, Strong Normalisation of Cut-Elimination That Simulates β-Reduction, Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus, Representing scope in intuitionistic deductions, Permutability of proofs in intuitionistic sequent calculi, Termination of permutative conversions in intuitionistic Gentzen calculi, Intersection Types for the Resource Control Lambda Calculi, On the intuitionistic force of classical search, Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation, On the Computational Representation of Classical Logical Connectives, Varieties of linear calculi
