A PolyTime Functional Language from Light Linear Logic

Patrick Baillot; Marco Gaboardi; Virgile Mogbil

hal-00443944, version 1

A PolyTime Functional Language from Light Linear Logic

Patrick Baillot () ¹, Marco Gaboardi () ², Virgile Mogbil () ³

19th European Symposium on Programming (ESOP 2010) 6012 (2010) pp. 104-124

Abstract: We introduce a typed functional programming language LPL (acronym for Light linear Programming Language) in which all valid programs run in polynomial time, and which is complete for polynomial time functions. LPL is based on lambda-calculus, with constructors for algebraic data-types, pattern matching and recursive definitions, and thus allows for a natural programming style. The validity of LPL programs is checked through typing and a syntactic criterion on recursive definitions. The higher order type system is designed from the ideas of Light linear logic: stratification, to control recursive calls, and weak exponential connectives §, !, to control duplication of arguments.

1: Laboratoire de l'Informatique du Parallélisme (LIP)
Université de Lyon – CNRS : UMR5668 – INRIA – École Normale Supérieure - Lyon – Université Claude Bernard - Lyon I
2: Dipartimento di Informatica [Torino]
Università di Torino
3: Laboratoire d'informatique de Paris-nord (LIPN)
CNRS : UMR7030 – Université Paris XIII - Paris Nord

hal-00443944, version 1
http://hal.archives-ouvertes.fr/hal-00443944
oai:hal.archives-ouvertes.fr:hal-00443944
From: Virgile Mogbil <>
Submitted on: Tuesday, 5 January 2010 11:14:01
Updated on: Friday, 1 April 2011 23:47:25

See detailed view

Associated documents

PDF :

DOI: 10.1007/978-3-642-11957-6

Export

Bibtex EndNote TEI RefWorks

%% hal-00443944, version 1
%% http://hal.archives-ouvertes.fr/hal-00443944
@inproceedings{baillot:hal-00443944,
    hal_id = {hal-00443944},
    url = {http://hal.archives-ouvertes.fr/hal-00443944},
    title = {{A PolyTime Functional Language from Light Linear Logic}},
    author = {Baillot, Patrick and Gaboardi, Marco and Mogbil, Virgile},
    abstract = {{We introduce a typed functional programming language LPL (acronym for Light linear Programming Language) in which all valid programs run in polynomial time, and which is complete for polynomial time functions. LPL is based on lambda-calculus, with constructors for algebraic data-types, pattern matching and recursive definitions, and thus allows for a natural programming style. The validity of LPL programs is checked through typing and a syntactic criterion on recursive definitions. The higher order type system is designed from the ideas of Light linear logic: stratification, to control recursive calls, and weak exponential connectives §, !, to control duplication of arguments.}},
    keywords = {Functional Language ; Light linear logic ; Polynomial Time ; Implicit Computational Complexity ; Type System},
    language = {English},
    affiliation = {Laboratoire de l'Informatique du Parall{\'e}lisme - LIP , Dipartimento di Informatica [Torino] , Laboratoire d'informatique de Paris-nord - LIPN},
    booktitle = {{Programming Languages and Systems 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings}},
    publisher = {Springer Berlin / Heidelberg},
    pages = {pp. 104-124},
    address = {Paphos, Cyprus},
    volume = {6012},
    editor = {Andrew D. Gordon },
    number = {6012 },
    series = {Lecture Notes in Computer Science },
    note = {30 pages rapport interne LIPN rapport interne LIPN },
    audience = {international },
    doi = {10.1007/978-3-642-11957-6 },
    year = {2010},
    month = Mar,
    pdf = {http://hal.archives-ouvertes.fr/hal-00443944/PDF/lpl\_preprintLIPN10.pdf},
}

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="hal-00443944"><analytic>
<author><persName><forename>Patrick</forename><surname>Baillot</surname></persName>
<affiliation>
<orgName type="laboratory">LIP</orgName>
<orgName type="team">Laboratoire de l'Informatique du Parallélisme</orgName>
<country>FR</country>
<orgName type="institution">Université de Lyon</orgName>
<orgName type="institution">CNRS : UMR5668</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">École Normale Supérieure - Lyon</orgName>
<orgName type="institution">Université Claude Bernard - Lyon I</orgName>
</affiliation>
</author>
<author><persName><forename>Marco</forename><surname>Gaboardi</surname></persName>
<affiliation>
<orgName type="team">Dipartimento di Informatica [Torino]</orgName>
<country>IT</country>
<orgName type="institution">Università di Torino</orgName>
</affiliation>
</author>
<author><persName><forename>Virgile</forename><surname>Mogbil</surname></persName>
<affiliation>
<orgName type="laboratory">LIPN</orgName>
<orgName type="team">Laboratoire d'informatique de Paris-nord</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7030</orgName>
<orgName type="institution">Université Paris XIII - Paris Nord</orgName>
</affiliation>
</author>
<title type="main" level="a">A PolyTime Functional Language from Light Linear Logic</title></analytic><monogr><title level="m" type="main">Programming Languages and Systems 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings</title><meeting>19th European Symposium on Programming (ESOP 2010)</meeting><imprint><publisher>Springer Berlin / Heidelberg</publisher><pubPlace><settlement>Paphos</settlement><country>Cyprus</country></pubPlace><biblScope type="publicationDate">2010-03-10</biblScope><biblScope type="vol">6012</biblScope><biblScope type="issue">6012</biblScope><biblScope type="pp">pp. 104-124</biblScope></imprint></monogr><idno type="doi">10.1007/978-3-642-11957-6</idno><idno type="HALid">http://hal.archives-ouvertes.fr/hal-00443944</idno><idno type="HALFile">http://hal.archives-ouvertes.fr/hal-00443944/PDF/lpl_preprintLIPN10.pdf</idno></biblStruct>
</listBibl>
</listBibl>