Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

A tier-based typed programming language characterizing Feasible Functionals

Emmanuel Hainry 1 Bruce Kapron 2 Jean-yves Marion 3 Romain Péchoux 1 
1 MOCQUA - Designing the Future of Computational Models
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 CARBONE - Carbone
LORIA - FM - Department of Formal Methods
Abstract : The class of Basic Feasible Functionals BFF 2 is the type-2 counterpart of the class FP of type-1 functions computable in polynomial time. Several characterizations have been suggested in the literature, but none of these present a programming language with a type system guaranteeing this complexity bound. We give a characterization of BFF 2 based on an imperative language with oracle calls using a tier-based type system whose inference is decidable. Such a characterization should make it possible to link higher-order complexity with programming theory. The low complexity (cubic in the size of the program) of the type inference algorithm contrasts with the intractability of the aforementioned methods and does not restrain strongly the expressive power of the language.
Document type :
Conference papers
Complete list of metadata

Cited literature [39 references]  Display  Hide  Download
Contributor : Emmanuel Hainry Connect in order to contact the contributor
Submitted on : Thursday, June 25, 2020 - 3:39:46 PM
Last modification on : Sunday, June 26, 2022 - 2:51:02 AM


Files produced by the author(s)




Emmanuel Hainry, Bruce Kapron, Jean-yves Marion, Romain Péchoux. A tier-based typed programming language characterizing Feasible Functionals. LICS '20 - 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken, Germany. pp.535-549, ⟨10.1145/3373718.3394768⟩. ⟨hal-02881308⟩



Record views


Files downloads