scientific article

No author found.

Publication date: 17 September 1992

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

cut elimination sequent calculus linear logic natural deduction proof normalization $\lambda $ -calculus coherence semantics

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Structure of proofs (03F07) Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)

Related Items

Simple type inference for term graph rewriting systems, Normalization in the simply typed -calculus, Linear domains and linear maps, YET ANOTHER FUZZY MODEL FOR LINEAR LOGIC, Unnamed Item, Unnamed Item, A Survey of the Proof-Theoretic Foundations of Logic Programming, Programming with streams in Coq a case study: The Sieve of Eratosthenes, A short and flexible proof of strong normalization for the calculus of constructions, Combinatorial flows as bicolored atomic flows, Type inference for rank-2 intersection types using set unification, Information links in domain theory, A Formal Proof of the Strong Normalization Theorem for System T in Agda, Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts, Classical (co)recursion: Mechanics, Complementary proof nets for classical logic, The elimination of maximum cuts in linear logic and BCK logic, The conservation theorem for differential nets, Constructive forcing, CPS translations and witness extraction in Interactive realizability, Classical realizability and arithmetical formulæ, UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC, Natural deduction calculi for classical and intuitionistic S5, An intuitionistic set-theoretical model of fully dependent CC, Game semantics of Martin-Löf type theory, Towards an induction principle for nested data types, Core Type Theory, Well-founded recursion with copatterns and sized types, The calculus of dependent lambda eliminations, Unnamed Item, Universal properties for universal types in bifibrational parametricity, A model of guarded recursion with clock synchronisation, Bifibrational functorial semantics of parametric polymorphism, Implicative algebras: a new foundation for realizability and forcing, Logic and Geometry of Agents in Agent-Based Modeling, Proof Terms for Generalized Natural Deduction, Various Constructions of Continuous Information Systems, Proofs as Polynomials, Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1, On the reification of semantic linearity, Relating reasoning methodologies in linear logic and process algebra, A Type-Theoretic Approach to Resolution, On the semantics of classical disjunction, On phase semantics and denotational semantics: The exponentials, Strong normalizability of the non-deterministic catch/throw calculi, The Role of Structural Reasoning in the Genesis of Graph Theory, On intuitionistic query answering in description bases, Decidable higher-order unification problems, Prawitz, Proofs, and Meaning, General-Elimination Harmony and Higher-Level Rules, Harmony in Proof-Theoretic Semantics: A Reductive Analysis, Monoidal-closed categories of tree automata, Unnamed Item, Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation, Implicit computation complexity in higher-order programming languages, On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem, A semantical proof of the strong normalization theorem for full propositional classical natural deduction, J-Calc: a typed lambda calculus for intuitionistic justification logic, Computation by interaction for space-bounded functional programming, Category theory, logic and formal linguistics: some connections, old and new, Atomicity, coherence of information, and point-free structures, Proofs as processes, On the $\pi$-calculus and linear logic, Coq formalization of the higher-order recursive path ordering, Adequacy for a lazy functional language with recursive and polymorphic types, Strong normalization for non-structural subtyping via saturated sets, Directly reflective meta-programming, Hypersequents, logical consequence and intermediate logics for concurrency, Simplifying proofs in Fitch-style natural deduction systems, Normalization results for typeable rewrite systems, Strong normalization from weak normalization in typed $\lambda$-calculi, An effective proof of the well-foundedness of the multiset path ordering, A (restricted) quantifier elimination for security protocols, Innovations in computational type theory using Nuprl, A decidable theory of type assignment, Strong normalisation in the $\pi$-calculus, Embedding of a free cartesian-closed category into the category of sets, The Girard-Reynolds isomorphism (second edition), Geometric construction by assembling solved subfigures, Intuitionistic completeness of first-order logic, Covariant types, Abstract data type systems, The definition of Extended ML: A gentle introduction, Higher-order subtyping, Nominal abstraction, The faithfulness of $\mathbf{F_{at}}$: a proof-theoretic proof, Typed operational semantics for higher-order subtyping., Proof theory of higher-order equations: Conservativity, normal forms and term rewriting., Classical logic with partial functions, Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control, A constructive analysis of learning in Peano arithmetic, Set systems: order types, continuous nondeterministic deformations, and quasi-orders, A binary modal logic for the intersection types of lambda-calculus., Linearity and iterator types for Gödel's system $\mathcal T$, Nominal techniques in Isabelle/HOL, Theorem proving modulo, Inheritance as implicit coercion, On strong normalization and type inference in the intersection type discipline, The heart of intersection type assignment: Normalisation proofs revisited, A typed lambda calculus with intersection types, Metacircularity in the polymorphic $\lambda$-calculus, Coherence spaces are untopological, Finite type structures within combinatory algebras, Soft linear set theory, Intersection type assignment systems with higher-order algebraic rewriting, Towards a proof theory of rewriting: The simply typed $2\lambda$-calculus, The complexity of higher-order queries, On maximal stable functions, Uniformity and the Taylor expansion of ordinary lambda-terms, The seven virtues of simple type theory, Decision problems for propositional linear logic, New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic, Bounded linear logic: A modular approach to polynomial-time computability, On the adequacy of representing higher order intuitionistic logic as a pure type system, Genetic programming $+$ proof search $=$ automatic improvement, The logic of structures, Prior's tonk, notions of logic, and levels of inconsistency: vindicating the pluralistic unity of science in the light of categorical logical positivism, Computing the Lagrangians of the standard model II. The ghost term, Comparing Hagino's categorical programming language and typed lambda- calculi, Computational interpretations of linear logic, Existential instantiation and normalization in sequent natural deduction, Gödel's system $\mathcal T$ revisited, The vectorial $\lambda$-calculus, Yet another bijection between sequent calculus and natural deduction, Preface to the special volume, Musings around the geometry of interaction, and coherence, Realizability models and implicit complexity, 2-sequent calculus: A proof theory of modalities, The undecidability of pattern matching in calculi where primitive recursive functions are representable, Constructive logics. I: A tutorial on proof systems and typed $\lambda$- calculi, Linearizing intuitionistic implication, On the membership problem for non-linear abstract categorial grammars, A faithful representation of non-associative Lambek grammars in abstract categorial grammars, Polarized and focalized linear and classical proofs, Cut-elimination in the strict intersection type assignment system is strongly normalizing, Typing termination in a higher-order concurrent imperative language, Representation and duality of the untyped $\lambda$-calculus in nominal lattice and topological semantics, with a proof of topological completeness, Pedagogical second-order $\lambda $-calculus, Types as graphs: Continuations in type logical grammar, First-order Glue, Structures definable in polymorphism, Intuitionistic hybrid logic: introduction and survey, Strong normalization of $\mathsf{ML}^{\mathsf F}$ via a calculus of coercions, Inductive proof search modulo, Commuting conversions vs. the standard conversions of the ``good connectives, Predicative functionals and an interpretation of ${\widehat{\text{ID}}_{<\omega}}$, Typability and type checking in System F are equivalent and undecidable, Gentzen-type systems, resolution and tableaux, Formal parametric polymorphism, The genericity theorem and parametricity in the polymorphic $\lambda$- calculus, Systems of combinatory logic related to Quine's `New Foundations', Informational interpretation of substructural propositional logics, Synthesis of ML programs in the system Coq, Towards a semantic characterization of cut-elimination, Structuring co-constructive logic for proofs and refutations, Characteristic bisimulation for higher-order session processes, Logic and majority voting, A computable expression of closure to efficient causation, Rasiowa-Harrop disjunction property, Self-quotation in a typed, intensional lambda-calculus, A simple sequent calculus for partial functions, The Church-Rosser theorem and quantitative analysis of witnesses, The Girard-Reynolds isomorphism, Logical foundations for hybrid type-logical grammars, Operational semantics of resolution and productivity in Horn clause logic, The naturality of natural deduction, Simply typed lambda calculus with first-class environments, Combinatory logic with polymorphic types, From realizability to induction via dependent intersection, Nominal essential intersection types, Set theory for verification. II: Induction and recursion, Strongly typed term representations in Coq, Relations and non-commutative linear logic, An approach to literate and structured formal developments, Linear Läuchli semantics, Polymorphic extensions of simple type structures. With an application to a bar recursive minimization, Linear logic automata, Differential logical relations. II: Increments and derivatives, Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels, Strong normalization and typability with intersection types, Some general results about proof normalization, A refined interpretation of intuitionistic logic by means of atomic polymorphism, Typing total recursive functions in Coq, Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications, A categorical model of predicate linear logic, Linear logic in computer science, A semantic framework for proof evidence, Cut elimination for a logic with induction and co-induction, Adding logic to the toolbox of molecular biology, Paraconsistency in classical logic, On phase semantics and denotational semantics in multiplicative-additive linear logic, Intensional computation with higher-order functions, Graded modal dependent type theory, Explicit Provability and Constructive Semantics, Natural deduction bottom up, On the Unusual Effectiveness of Logic in Computer Science, Strong normalization through intersection types and memory, The polarized $\lambda$-calculus, Polynomial time in untyped elementary linear logic, On the concurrent computational content of intermediate logics, Full abstraction for polymorphic $\pi $-calculus, Towards a more general concept of inference, Normal proofs, cut free derivations and structural rules, Les types de données syntaxiques du système ${\cal F}$, LesI-types du système ${\cal F}$, A stable programming language, Regaining cut admissibility in deduction modulo using abstract completion, A game semantics for generic polymorphism, Comments on predicative logic, Abstract canonical presentations, Relating categorical semantics for intuitionistic linear logic, A categorical construction for the computational definition of vector spaces, Investigations on the dual calculus, Intuitionistic hybrid logic, An Interaction Net Encoding of Gödel’s System $$\mathcal {T}$$, Proof Relevant Corecursive Resolution, What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics, Steps and traces, Atomic polymorphism and the existence property, Logical Semantics for Stability, Abstracting models of strong normalization for classical calculi, Generating plans in linear logic. I: Actions as proofs, Models of linear logic, A Curry–Howard View of Basic Justification Logic, A unary representation result for system $T$, Curry-Howard-Lambek correspondence for intuitionistic belief, Poset-valued sets or how to build models for linear logics, Soft linear logic and polynomial time, On the intuitionistic force of classical search, Strongly Normalising Cut-Elimination with Strict Intersection Types, A simple proof of second-order strong normalization with permutative conversions, Natural deduction for quantum logic, Linear numeral systems, From computation to foundations via functions and application: The $\lambda$-calculus and its webbed models, Extended Curry-Howard terms for second-order logic, Order-enriched categorical models of the classical sequent calculus, Confluency and strong normalizability of call-by-value $\lambda \mu$-calculus, Bisimilarity of open terms., Type destructors, Objects and classes in Algol-like languages, Assigning types to processes, Intersection and singleton type assignment characterizing finite Böhm-trees, A structural approach to reversible computation, Conformal Field Theory as a Nuclear Functor, Syntactic Logical Relations for Polymorphic and Recursive Types, Light Dialectica Program Extraction from a Classical Fibonacci Proof, Relational model of second order linear logic, Corecursion up-to via causal transformations, Tool Support for Proof Engineering, Normalization for the Simply-Typed Lambda-Calculus in Twelf, Logical optimality of groundness analysis, Minimality in a Linear Calculus with Iteration, An alternative normalization of the implicative fragment of classical logic, Equational rules for rewriting logic, The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives, Explicit effect subtyping, Upper bounds for standardizations and an application, The shuffle Hopf algebra and noncommutative full completeness, Strongly-Normalizing Higher-Order Relational Queries, Types as parameters, On Type Coercion in Compositional and Lexical Semantics, A combinatory account of internal structure, On confluence for weakly normalizing systems, (Head-)normalization of typeable rewrite systems, Understanding Game Semantics Through Coherence Spaces, Continuation Models for the Lambda Calculus With Constructors, Proof-Search in Natural Deduction Calculus for Classical Propositional Logic, An Analytic Propositional Proof System on Graphs, The Rule of Existential Generalisation and Explicit Substitution, Theorems as Constructive Visions, Unnamed Item, Unnamed Item, Unnamed Item, About some symmetries of negation, IX Latin American Symposium on Mathematical Logic, Bahía Blanca, 1992, Transport of finiteness structures and applications, A natural deduction system for bundled branching time logic, Structural Focalization, Parametricity of extensionally collapsed term models of polymorphism and their categorical properties, Parametric Polymorphism — Universally, Intuitive counterexamples for constructive fallacies, Judgement aggregation in non-classical logics, Extending the Curry-Howard interpretation to linear, relevant and other resource logics, Contraction-free sequent calculi for intuitionistic logic, Elementary Proof of Strong Normalization for Atomic F, Normal forms, linearity, and prime algebraicity over nonflat domains, How to prove decidability of equational theories with second-order computation analyser SOL, POPLMark reloaded: Mechanizing proofs by logical relations, A complete characterization of primitive recursive intensional behaviours, Tight typings and split bounds, fully developed, Unnamed Item, Unnamed Item, Specifying Peirce's law in classical realizability, Three faces of natural deduction, On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC, Unnamed Item, Unnamed Item, Unnamed Item, From Qualitative to Quantitative Semantics, On Higher-Order Probabilistic Subrecursion, Probabilistic Termination by Monadic Affine Sized Typing, Unnamed Item, Unnamed Item, Syntactic Metatheory of Higher-Order Subtyping, Cofree coalgebras and differential linear logic, A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object, Modularity of termination and confluence in combinations of rewrite systems with λω, The Impact of the Lambda Calculus in Logic and Computer Science, Bistructures, bidomains and linear logic, Can a Quantum Computer Run the von Neumann Architecture?, POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE, Unnamed Item, Validating Brouwer's continuity principle for numbers using named exceptions, Linear Lambda Calculus and Deep Inference, A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits, Approximation and normalization results for typeable term rewriting systems, Two different strong normalization proofs?, Third-order matching in the polymorphic lambda calculus, Reflection of formal tactics in a deductive reflection framework, Reflection principles for synthetic theories of smooth manifolds, Strong normalization proof with CPS-translation for second order classical natural deduction, Proof normalization modulo, Identity of Proofs Based on Normalization and Generality, Proofs of strong normalisation for second order classical natural deduction, Narrowing Based Inductive Proof Search, Atomic polymorphism, Résultats de complétude pour des classes de types du système $\mathcal {AF}2$, Une réponse négative à la conjecture de E. Tronci pour les systèmes numériques typés, The emptiness problem for intersection types, Unnamed Item, Unnamed Item, Monotone (co)inductive types and positive fixed-point types, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, On the non-confluence of cut-elimination, Unnamed Item, Unnamed Item, FRACTIONAL SEMANTICS FOR CLASSICAL LOGIC, Static Livelock Analysis in CSP, Relating Classical Realizability and Negative Translation for Existential Witness Extraction, A Polymorphic Type System for the Lambda-Calculus with Constructors, Opérateurs de mise en mémoire et types $\forall $-positifs, Typed Applicative Structures and Normalization by Evaluation for System F ω, Programs with continuations and linear logic, Unnamed Item, Dynamic game semantics, Two extensions of system F with (co)iteration and primitive (co)recursion principles, Automating Theories in Intuitionistic Logic, The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type, Aspects of Categorical Recursion Theory, Lilac: a functional programming language based on linear logic, Propositions as sessions