10 Search Results for "Terui, Kazushige"

Document
DOI: 10.4230/LIPIcs.CSL.2026.17
A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials

Authors: Alexis Saurin and Esaïe Bauer

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
In the realm of light logics deriving from linear logic, a number of variants of exponential rules have been investigated. The profusion of such proof systems induces the need for cut-elimination theorems for each logic, the proofs of which may be redundant. A number of approaches in proof theory have been adopted to cope with this need. In the present paper, we consider this issue from the point of view of enhancing linear logic with least and greatest fixed-points and considering such a variety of exponential connectives. Our main contribution is to provide a uniform cut-elimination theorem for a parametrized system with fixed-points by combining two approaches: cut-elimination proofs by reduction (or translation) to another system and the identification of sufficient conditions for cut-elimination. More precisely, we examine a broad range of systems, taking inspiration from Nigam and Miller’s subexponentials and from the first author and Laurent’s super exponentials. Our work is motivated, on the one hand, by Baillot’s work on light logics with recursive types and on the other hand by our recent work on the proof theory of the modal μ-calculus.
Cite as

Alexis Saurin and Esaïe Bauer. A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 17:1-17:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{saurin_et_al:LIPIcs.CSL.2026.17,
  author =	{Saurin, Alexis and Bauer, Esa\"{i}e},
  title =	{{A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{17:1--17:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.17},
  URN =		{urn:nbn:de:0030-drops-254418},
  doi =		{10.4230/LIPIcs.CSL.2026.17},
  annote =	{Keywords: cut elimination, exponential modalities, fixed-points, linear logic, light logics, mu-calculus, non-wellfounded proofs, proof theory, sequent calculus, subexponentials, super exponentials}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.32
Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation

Authors: Alexis Saurin

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Analyzing Maehara’s method for proving Craig’s interpolation theorem, we extract a "proof relevant" interpolation theorem for first-order LL in the sense that if π is a cut-free sequent proof of A⊢ B, we can find a formula C in the common vocabulary of A and B and proofs π₁,π₂ of A⊢ C and C⊢ B respectively such that π₁ composed with π₂ cut-reduces to π. As a direct corollary, we get similar proof relevant interpolation results for LJ and LK using linear translations. This refined interpolation is then rephrased in terms of a cut-introduction process synthetizing the interpolant. Finally, we analyze the computational content of interpolation by proving an interpolation result for Curien and Herbelin’s Duality of Computation.
Cite as

Alexis Saurin. Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 32:1-32:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{saurin:LIPIcs.FSCD.2025.32,
  author =	{Saurin, Alexis},
  title =	{{Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{32:1--32:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.32},
  URN =		{urn:nbn:de:0030-drops-236478},
  doi =		{10.4230/LIPIcs.FSCD.2025.32},
  annote =	{Keywords: Classical Logic, Interpolation, Cut Elimination, Linear Logic, Sequent calculus, System L}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.170
First-Order Intuitionistic Linear Logic and Hypergraph Languages

Authors: Tikhon Pshenitsyn

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
The Lambek calculus is a substructural logic known to be closely related to the formal language theory: on the one hand, it is used for generating formal languages by means of categorial grammars and, on the other hand, it has formal language semantics, with respect to which it is sound and complete. This paper studies a similar relation between first-order intuitionistic linear logic ILL1 along with its multiplicative fragment MILL1 on the one hand and the hypergraph grammar theory on the other. In the first part, we introduce a novel concept of hypergraph first-order logic categorial grammar, which is a generalisation of string MILL1 grammars introduced in Richard Moot’s works. We prove that hypergraph ILL1 grammars generate all recursively enumerable hypergraph languages and that hypergraph MILL1 grammars are as powerful as linear-time hypergraph transformation systems. In addition, we show that the class of languages generated by string MILL1 grammars is closed under intersection and that it includes a non-semilinear language as well as an NP-complete one. This shows how much more powerful string MILL1 grammars are as compared to Lambek categorial grammars. In the second part, we develop hypergraph language models for MILL1. In such models, formulae of the logic are interpreted as hypergraph languages and multiplicative conjunction is interpreted using parallel composition, which is one of the operations of HR-algebras introduced by Courcelle. We prove completeness of the universal-implicative fragment of MILL1 with respect to these models and thus present a new kind of semantics for a fragment of first-order linear logic.
Cite as

Tikhon Pshenitsyn. First-Order Intuitionistic Linear Logic and Hypergraph Languages. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 170:1-170:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{pshenitsyn:LIPIcs.ICALP.2025.170,
  author =	{Pshenitsyn, Tikhon},
  title =	{{First-Order Intuitionistic Linear Logic and Hypergraph Languages}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{170:1--170:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.170},
  URN =		{urn:nbn:de:0030-drops-235473},
  doi =		{10.4230/LIPIcs.ICALP.2025.170},
  annote =	{Keywords: linear logic, categorial grammar, MILL1 grammar, first-order logic, hypergraph language, graph transformation, language semantics, HR-algebra}
}
Document
DOI: 10.4230/LIPIcs.CSL.2024.42
Local Operators in Topos Theory and Separation of Semi-Classical Axioms in Intuitionistic Arithmetic

Authors: Satoshi Nakata

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
There has been work on the strength of semi-classical axioms over Heyting arithmetic such as Σ_n-DNE (double negation elimination) and Π_n-LEM (law of excluded middle). Among other things, Akama et al. show that Σ_n-DNE does not imply Π_n-LEM for any n ≥ 1 by using Kleene realizability relativized to Turing degrees. These realizability notions are expressed by subtoposes of the effective topos ℰff and thus by corresponding local operators (a.k.a. Lawvere-Tierney topologies). Our purpose is to provide a topos-theoretic explanation for separation of semi-classical axioms. It consists of determining the least dense local operator of a given axiom φ in a topos ℰ, which completely characterizes the dense subtoposes of ℰ satisfying φ. This idea is motivated by Caramello’s study of intermediate propositional logics and van Oosten’s study of Lifschitz realizability. We first investigate sufficient conditions for an arithmetical formula to have a least dense operator. In particular, we show that each semi-classical axiom has a least dense operator in every elementary topos with natural number object. This is a generalization of van Oosten’s result for Π₁∨Π₁-DNE in ℰff. We next determine least dense operators of semi-classical axioms in ℰff in terms of (generalized) Turing degrees. Not only does it immediately imply some separation results of Akama et al. but also explain that realizability notions they used are optimal in the sense of minimality. We finally point out a negative consequence that Π_n-LEM, Σ_n-LEM and Σ_{n+1}-DNE are never separable by any subtopos of ℰff for any n ≥ 0.
Cite as

Satoshi Nakata. Local Operators in Topos Theory and Separation of Semi-Classical Axioms in Intuitionistic Arithmetic. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 42:1-42:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{nakata:LIPIcs.CSL.2024.42,
  author =	{Nakata, Satoshi},
  title =	{{Local Operators in Topos Theory and Separation of Semi-Classical Axioms in Intuitionistic Arithmetic}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{42:1--42:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.42},
  URN =		{urn:nbn:de:0030-drops-196859},
  doi =		{10.4230/LIPIcs.CSL.2024.42},
  annote =	{Keywords: local operator, elementary topos, effective topos, realizability, intuitionistic arithmetic}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.123
From Normal Functors to Logarithmic Space Queries (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Lê Thành Dũng Nguyễn and Cécilia Pradic

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
We introduce a new approach to implicit complexity in linear logic, inspired by functional database query languages and using recent developments in effective denotational semantics of polymorphism. We give the first sub-polynomial upper bound in a type system with impredicative polymorphism; adding restrictions on quantifiers yields a characterization of logarithmic space, for which extensional completeness is established via descriptive complexity.
Cite as

Lê Thành Dũng Nguyễn and Cécilia Pradic. From Normal Functors to Logarithmic Space Queries (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 123:1-123:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{nguyen_et_al:LIPIcs.ICALP.2019.123,
  author =	{Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng and Pradic, C\'{e}cilia},
  title =	{{From Normal Functors to Logarithmic Space Queries}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{123:1--123:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.123},
  URN =		{urn:nbn:de:0030-drops-106994},
  doi =		{10.4230/LIPIcs.ICALP.2019.123},
  annote =	{Keywords: coherence spaces, elementary linear logic, semantic evaluation}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.20
A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4

Authors: Yosuke Fukuda and Akira Yoshimizu

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We propose a modal linear logic to reformulate intuitionistic modal logic S4 (IS4) in terms of linear logic, establishing an S4-version of Girard translation from IS4 to it. While the Girard translation from intuitionistic logic to linear logic is well-known, its extension to modal logic is non-trivial since a naive combination of the S4 modality and the exponential modality causes an undesirable interaction between the two modalities. To solve the problem, we introduce an extension of intuitionistic multiplicative exponential linear logic with a modality combining the S4 modality and the exponential modality, and show that it admits a sound translation from IS4. Through the Curry-Howard correspondence we further obtain a Geometry of Interaction Machine semantics of the modal lambda-calculus by Pfenning and Davies for staged computation.
Cite as

Yosuke Fukuda and Akira Yoshimizu. A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 20:1-20:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{fukuda_et_al:LIPIcs.FSCD.2019.20,
  author =	{Fukuda, Yosuke and Yoshimizu, Akira},
  title =	{{A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{20:1--20:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.20},
  URN =		{urn:nbn:de:0030-drops-105271},
  doi =		{10.4230/LIPIcs.FSCD.2019.20},
  annote =	{Keywords: linear logic, modal logic, Girard translation, Curry-Howard correspondence, geometry of interaction, staged computation}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.37
MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics

Authors: Kazushige Terui

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Buchholz' Omega-rule is a way to give a syntactic, possibly ordinal-free proof of cut elimination for various subsystems of second order arithmetic. Our goal is to understand it from an algebraic point of view. Among many proofs of cut elimination for higher order logics, Maehara and Okada's algebraic proofs are of particular interest, since the essence of their arguments can be algebraically described as the (Dedekind-)MacNeille completion together with Girard's reducibility candidates. Interestingly, it turns out that the Omega-rule, formulated as a rule of logical inference, finds its algebraic foundation in the MacNeille completion. In this paper, we consider a family of sequent calculi LIP = cup_{n >= -1} LIP_n for the parameter-free fragments of second order intuitionistic logic, that corresponds to the family ID_{<omega} = cup_{n <omega} ID_n of arithmetical theories of inductive definitions up to omega. In this setting, we observe a formal connection between the Omega-rule and the MacNeille completion, that leads to a way of interpreting second order quantifiers in a first order way in Heyting-valued semantics, called the Omega-interpretation. Based on this, we give a (partly) algebraic proof of cut elimination for LIP_n, in which quantification over reducibility candidates, that are genuinely second order, is replaced by the Omega-interpretation, that is essentially first order. As a consequence, our proof is locally formalizable in ID-theories.
Cite as

Kazushige Terui. MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{terui:LIPIcs.CSL.2018.37,
  author =	{Terui, Kazushige},
  title =	{{MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{37:1--37:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.37},
  URN =		{urn:nbn:de:0030-drops-97049},
  doi =		{10.4230/LIPIcs.CSL.2018.37},
  annote =	{Keywords: Algebraic cut elimination, Parameter-free second order logic, MacNeille completion, Omega-rule}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.5
Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.

Authors: Ryota Akiyoshi and Kazushige Terui

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
Following Aehlig, we consider a hierarchy F^p= { F^p_n }_{n in Nat} of parameter-free subsystems of System F, where each F^p_n corresponds to ID_n, the theory of n-times iterated inductive definitions (thus our F^p_n corresponds to the n+1th system of Aehlig). We here present two proofs of strong normalization for F^p_n, which are directly formalizable with inductive definitions. The first one, based on the Joachimski-Matthes method, can be fully formalized in ID_n+1. This provides a tight upper bound on the complexity of the normalization theorem for System F^p_n. The second one, based on the Godel-Tait method, can be locally formalized in ID_n. This provides a direct proof to the known result that the representable functions in F^p_n are provably total in ID_n. In both cases, Buchholz' Omega-rule plays a central role.
Cite as

Ryota Akiyoshi and Kazushige Terui. Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{akiyoshi_et_al:LIPIcs.FSCD.2016.5,
  author =	{Akiyoshi, Ryota and Terui, Kazushige},
  title =	{{Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{5:1--5:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.5},
  URN =		{urn:nbn:de:0030-drops-59718},
  doi =		{10.4230/LIPIcs.FSCD.2016.5},
  annote =	{Keywords: Polymorphic Lambda Calculus, Strong Normalization, Computability Predicate, Infinitary Proof Theory}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2013.41
Intersection Types for Normalization and Verification (Invited Talk)

Authors: Kazushige Terui

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)

Abstract
One of the basic principles in typed lambda calculi is that typable lambda terms are normalizable. Since the converse direction does not hold for simply typed lambda calculus, people have been studying its extensions. This gave birth to the intersection type systems, that exactly characterize various classes of lambda terms, such as strongly/weakly normalizable terms and solvable ones (see e.g. [van Bakel/TCS/1995] for a survey). More recently, a new trend has emerged: intersection types are not only useful for extending simple types but also for refining them [Salvati/JoLLI/2010]. One thus obtains finer information on simply typed terms by assigning intersection types. This in particular leads to the concept of normalization by typing, that turns out to be quite efficient in some situations [Terui/RTA/2012]. Moreover, intersection types are invariant under beta-equivalence, so that they constitute a denotational semantics in a natural way [Ehrhard/CSL/2012]. Finally, intersection types also work in an infinitary setting,where terms may represent infinite trees and types play the role of automata. This leads to a model checking framework for higher order recursion schemes via intersection types [Kobayashi/POPL/2009, Kobayashi+Luke Ong/LICS/2009]. The purpose of this talk is to outline the recent development of intersection types described above. In particular, we explain how an efficient evaluation algorithm is obtained by combining normalization by typing, beta-reduction and Krivine's abstract machine, to result in the following complexity characterization. Consider simply typed lambda terms of boolean type o -> o -> o and of order r. Then the problem of deciding whether a given term evaluates to "true" is complete for n-EXPTIME if r = 2n +2, and complete for n- EXPSPACE if r = 2n + 3 [Terui/RTA/2012].
Cite as

Kazushige Terui. Intersection Types for Normalization and Verification (Invited Talk). In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 41-42, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{terui:LIPIcs.FSTTCS.2013.41,
  author =	{Terui, Kazushige},
  title =	{{Intersection Types for Normalization and Verification}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{41--42},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.41},
  URN =		{urn:nbn:de:0030-drops-44032},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.41},
  annote =	{Keywords: simply typed lambda calculus, computational complexity, denotational semantics, intersection types}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.323
Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus

Authors: Kazushige Terui

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
Consider the following problem: given a simply typed lambda term of Boolean type and of order r, does it normalize to "true"? A related problem is: given a term M of word type and of order r together with a finite automaton D, does D accept the word represented by the normal form of M? We prove that these problems are n-EXPTIME complete for r=2n+2, and n-EXPSPACE complete for r=2n+3. While the hardness part is relatively easy, the membership part is not so obvious; in particular, simply applying beta reduction does not work. Some preceding works employ semantic evaluation in the category of sets and functions, but it is not efficient enough for our purpose. We present an algorithm for the above type of problem that is a fine blend of beta reduction, Krivine abstract machine and semantic evaluation in a category based on preorders and order ideals, also known as the Scott model of linear logic. The semantic evaluation can also be presented as intersection type checking.
Cite as

Kazushige Terui. Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 323-338, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{terui:LIPIcs.RTA.2012.323,
  author =	{Terui, Kazushige},
  title =	{{Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{323--338},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.323},
  URN =		{urn:nbn:de:0030-drops-35012},
  doi =		{10.4230/LIPIcs.RTA.2012.323},
  annote =	{Keywords: simply typed lambda calculus, computational complexity, denotational semantics, intersection types}
}
  • Refine by Type
  • 10 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 2 2025
  • 1 2024
  • 2 2019
  • 1 2018
  • Show More...

  • Refine by Author
  • 4 Terui, Kazushige
  • 2 Saurin, Alexis
  • 1 Akiyoshi, Ryota
  • 1 Bauer, Esaïe
  • 1 Fukuda, Yosuke
  • Show More...

  • Refine by Series/Journal
  • 10 LIPIcs

  • Refine by Classification
  • 5 Theory of computation → Linear logic
  • 4 Theory of computation → Proof theory
  • 1 Theory of computation → Complexity theory and logic
  • 1 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Finite Model Theory
  • Show More...

  • Refine by Keyword
  • 3 linear logic
  • 2 computational complexity
  • 2 denotational semantics
  • 2 intersection types
  • 2 simply typed lambda calculus
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact