Logical Combinators for Rich Type Systems

Pierre Genevès; Nabil Layaïda; Alan Schmitt

hal-00714353, version 2

Logical Combinators for Rich Type Systems

Pierre Genevès (, )^a^, 1, Nabil Layaïda ()^b^, 1, Alan Schmitt ()^b^, 2

N° RR-8010 (2012)

Résumé : We present a functional approach to design rich type systems based on an elegant logical representation of types. The representation is not only clean but avoids exponential increases in combined complexity due to subformula duplication. This opens the way for solving a wide range of problems such as subtyping in exponential-time even though their direct translation into the underlying logic results in an exponential blowup of the formula size, yielding an incorrectly presumed two-exponential time complexity.

a – CNRS
b – INRIA
1 : WAM (INRIA Grenoble Rhône-Alpes / LIG Laboratoire d'Informatique de Grenoble)
INRIA – Institut polytechnique de Grenoble (Grenoble INP) – Université Joseph Fourier - Grenoble I – Université Pierre-Mendès-France - Grenoble II – CNRS : UMR5217
2 : CELTIQUE (INRIA - IRISA)
INRIA – Université de Rennes 1 – École normale supérieure de Cachan - ENS Cachan – CNRS : UMR6074

hal-00714353, version 2
http://hal.inria.fr/hal-00714353
oai:hal.inria.fr:hal-00714353
Contributeur : Pierre Genevès <>
Soumis le : Mercredi 4 Juillet 2012, 12:01:26
Dernière modification le : Vendredi 6 Juillet 2012, 14:16:19

Voir la fiche détaillée

Documents associés

PDF :

Exporter

Bibtex EndNote TEI RefWorks

<?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="report"><head>Rapports</head>
<biblStruct type="report" xml:id="hal-00714353"><monogr>
<author><persName><forename>Pierre</forename><surname>Genevès</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Grenoble Rhône-Alpes / LIG Laboratoire d'Informatique de Grenoble</orgName>
<orgName type="team">WAM</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Institut polytechnique de Grenoble (Grenoble INP)</orgName>
<orgName type="institution">Université Joseph Fourier - Grenoble I</orgName>
<orgName type="institution">Université Pierre-Mendès-France - Grenoble II</orgName>
<orgName type="institution">CNRS : UMR5217</orgName>
</affiliation>
</author>
<author><persName><forename>Nabil</forename><surname>Layaïda</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Grenoble Rhône-Alpes / LIG Laboratoire d'Informatique de Grenoble</orgName>
<orgName type="team">WAM</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Institut polytechnique de Grenoble (Grenoble INP)</orgName>
<orgName type="institution">Université Joseph Fourier - Grenoble I</orgName>
<orgName type="institution">Université Pierre-Mendès-France - Grenoble II</orgName>
<orgName type="institution">CNRS : UMR5217</orgName>
</affiliation>
</author>
<author><persName><forename>Alan</forename><surname>Schmitt</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">CELTIQUE</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
<orgName type="institution">École normale supérieure de Cachan - ENS Cachan</orgName>
<orgName type="institution">CNRS : UMR6074</orgName>
</affiliation>
</author>
<title type="main" level="m">Logical Combinators for Rich Type Systems</title><title type="main" level="m">Logical Combinators for Rich Type Systems</title><imprint><biblScope type="publicationDate">2012-07-04</biblScope><biblScope type="pp">18</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/hal-00714353</idno><idno type="HALFile">http://hal.inria.fr/hal-00714353/PDF/RR-8010.pdf</idno></biblStruct>
</listBibl>
</listBibl>