Skip to Main content Skip to Navigation

Logical Combinators for Rich Type Systems

Pierre Genevès 1 Nabil Layaïda 1 Alan Schmitt 2 
1 WAM - Web, adaptation and multimedia
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : 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.
Document type :
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Pierre Genevès Connect in order to contact the contributor
Submitted on : Wednesday, July 4, 2012 - 12:01:26 PM
Last modification on : Tuesday, August 2, 2022 - 3:56:23 AM
Long-term archiving on: : Friday, March 31, 2017 - 10:12:17 AM


Files produced by the author(s)


  • HAL Id : hal-00714353, version 2


Pierre Genevès, Nabil Layaïda, Alan Schmitt. Logical Combinators for Rich Type Systems. [Research Report] RR-8010, INRIA. 2012, pp.18. ⟨hal-00714353v2⟩



Record views


Files downloads