scientific article; zbMATH DE number 512773
From MaRDI portal
Publication:4281466
zbMath0795.68127MaRDI QIDQ4281466
J. M. E. Hyland, Nick Benton, G. M. Bierman, V. C. V. de Paiva
Publication date: 7 April 1994
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
sequent calculusterm assignment systemGirard's intuitionistic linear logicnatural deduction proof systems
Semantics in the theory of computing (68Q55) Cut-elimination and normal-form theorems (03F05) Abstract deductive systems (03B22) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items
Linear Logic Properly Displayed, Coherence in SMCCs and equivalences on derivations in IMML with unit, A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types, Undecidability of Propositional Separation Logic and Its Neighbours, Resource operators for \(\lambda\)-calculus, Execution time of λ-terms via denotational semantics and intersection types, Non-normal modalities in variants of linear logic, New Curry-Howard terms for full linear logic, A general adequacy result for a linear functional language, Glueing and orthogonality for models of linear logic, A new framework for declarative programming, A linear logical framework, On categorical equivalence of Gentzen-style derivations in IMLL, Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic, Semantical analysis of contextual types, Unnamed Item, Unnamed Item, Unnamed Item, Focused linear logic and the \(\lambda\)-calculus, Encodings of Turing machines in linear logic, A model of intuitionistic affine logic from stable domain theory, Factorization in call-by-name and call-by-value calculi via linear logic, A linear/producer/consumer model of classical linear logic, Categories for computation in context and unified logic, Covert Movement in Logical Grammar, Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic, Synthetic domain theory and models of linear Abadi {\&} Plotkin logic, Type inference for light affine logic via constraints on words, A Type Theory for Probabilistic and Bayesian Reasoning, Relating categorical semantics for intuitionistic linear logic, Translations between Gentzen-Prawitz and Jaśkowski-Fitch natural deduction proofs, Proof theory in the abstract, Two applications of analytic functors, Unnamed Item, Intersection Types for the Resource Control Lambda Calculi, An implementation model of the typed λ-calculus based on Linear Chemical Abstract Machine, Weak linearization of the lambda calculus, A type- and scope-safe universe of syntaxes with binding: their semantics and proofs, Classical lambda calculus in modern dress, An internal language for autonomous categories
Uses Software
