scientific article

Publication date: 1987

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

abstract machine cut elimination sequent calculus lazy evaluation intuitionistic linear logic implementation of functional languages linear computations evaluation mechanism combinator system of course

Mathematics Subject Classification ID

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Related Items

Structured theory presentations and logic representations, Models of Linear Logic based on the Schwartz $\varepsilon$-product, Strong normalization of the second-order symmetric $\lambda \mu$-calculus, Holomorphic models of exponential types in linear logic, Model checking mobile ambients, Coherence in SMCCs and equivalences on derivations in IMML with unit, Proof of a S.Mac Lane conjecture (extended abstract), On completeness theorems for feature logics, Unnamed Item, Petri nets, Horn programs, linear logic and vector games, Back to futures, The linear abstract machine, Completeness results for linear logic on Petri nets, Undecidability of Propositional Separation Logic and Its Neighbours, Relations and non-commutative linear logic, A constructive topological proof of van der Waerden's theorem, Unnamed Item, Unnamed Item, Proof of a conjecture of S. Mac Lane, Linear Läuchli semantics, Linear logic automata, Quantitative domains, groupoids and linear logic, A general adequacy result for a linear functional language, Developing developments, Experiments in linear natural deduction, Unnamed Item, Additives of linear logic and normalization. I: A (restricted) Church-Rosser property., On categorical equivalence of Gentzen-style derivations in IMLL, Resource convertibility and ordered commutative monoids, Unnamed Item, Semantic Analysis of Subexponential Modalities in Distributive Non-commutative Linear Logic, A curry-style semantics of interaction: from untyped to second-order lazy $\lambda\mu$-calculus, Hintikka multiplicities in matrix decision methods for some propositional modal logics, Axioms and models of linear logic, Unnamed Item, Categorical interpretation of logical derivations and its applications in algebra, The geometry of tensor calculus. I, Linear logical relations and observational equivalences for session-based concurrency, A graphical foundation for interleaving in game semantics, Bistructures, bidomains and linear logic, Towards a clausal analysis of cut-elimination, Nested session types, On categorical aspects of $S$-quantales, Kleene star, subexponentials without contraction, and infinite computations, A decision procedure revisited: Notes on direct logic, linear logic and its implementation, Nonmodal classical linear predicate logic is a fragment of intuitionistic linear logic, Linear logic, coherence and dinaturality, $dI$--domains as prime information systems, Machine semantics, Syllogisms in rudimentary linear logic, diagrammatically, A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs, A representation theorem for quantales, Linearizing intuitionistic implication, Unnamed Item, Relating categorical semantics for intuitionistic linear logic, A semantic proof of polytime soundness of light affine logic, A message-passing interpretation of adjoint logic, Closures and Modules Within Linear Logic Concurrent Constraint Programming, Structural Analysis of Narratives with the Coq Proof Assistant, System $T$, call-by-value and the minimum problem, Mechanizing focused linear logic in Coq, Linear concurrent constraint programming: Operational and phase semantics, Dependent types with subtyping and late-bound overloading, Session typing and asynchronous subtyping for the higher-order $\pi$-calculus, Full intuitionistic linear logic, A uniform semantic proof for cut-elimination and completeness of various first and higher order logics., Simple consequence relations, The parametric continuation monad