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 :
Reports
Complete list of metadatas

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-00714353
Contributor : Pierre Genevès <>
Submitted on : Wednesday, July 4, 2012 - 12:01:26 PM
Last modification on : Wednesday, February 20, 2019 - 2:32:03 PM
Long-term archiving on : Friday, March 31, 2017 - 10:12:17 AM

File

RR-8010.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00714353, version 2

Citation

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

Share

Metrics

Record views

1435

Files downloads

435