License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2013.41
URN: urn:nbn:de:0030-drops-44032
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4403/
Go to the corresponding LIPIcs Volume Portal

Terui, Kazushige

Intersection Types for Normalization and Verification (Invited Talk)

pdf-format:
45.pdf (0.2 MB)

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].

BibTeX - Entry

@InProceedings{terui:LIPIcs:2013:4403,
  author =	{Kazushige Terui},
  title =	{{Intersection Types for Normalization and Verification (Invited Talk)}},
  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 =	{Anil Seth and Nisheeth K. Vishnoi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4403},
  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}
}

Keywords: simply typed lambda calculus, computational complexity, denotational semantics, intersection types
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)
Issue Date: 2013
Date of publication: 10.12.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI