COCA HOLA
Acronym: COst models for Complexity Analyses of Higher-Order LAnguages.
Principal Investigator: Beniamino Accattoli.
Collaborators: Ugo Dal Lago, Delia Kesner, Damiano Mazza, and Claudio Sacerdoti Coen.
The COCA HOLA project aims at developing complexity analyses of higher-order computations, i.e. that approach to computation where the inputs and outputs of a program are not simply numbers, strings, or compound data-types, but programs themselves. The focus is not on analysing fixed programs, but whole programming languages. The aim is the identification of adequate units of measurement for time and space, i.e. what are called reasonable cost models. The problem is non-trivial because the evaluation of higher-order languages is defined abstractly, via high-level operations, leaving the implementation unspecified. Concretely, the project will analyse different implementation schemes, measuring precisely their computational complexity with respect to the number of high-level operations, and eventually develop more efficient new ones. The goal is to obtain a complexity-aware theory of implementations of higher-order languages with both theoretical and practical downfalls.
The projects stems from recent advances on the theory of time cost models for the lambda-calculus, the computational model behind the higher-order approach, obtained by the principal investigator and his collaborators (who are included in the project).
COCA HOLA will span over three years and is organised around three work packages, essentially:
extending the current results to encompass realistic languages;
explore the gap between positive and negative results in the literature;
use ideas from linear logic to explore space cost models, about which almost nothing is known.
Documents
The project proposal. Note that the ANR did not fund all the demanded resources, in particular it did not fund the postdoc scholarship.
Papers
Journal papers:
Accattoli, Graham-Lengrand, Kesner. Tight Typings and Split Bounds, Fully Developed. Journal of Functional Programming 2020, special issue of ICFP 2018.
Accattoli, Guerrieri. Abstract Machines for Open Call-by-Value. Science of Computer Programming 2019, special issue of FSEN 2017.
Conferences with journal proceedings:
Accattoli, Dal Lago, Vanoni. The (In)Efficiency of Interaction. POPL 2021.
Accattoli, Graham-Lengrand, Kesner. Tight Typings and Split Bounds. ICFP 2018.
Conference proceedings:
Accattoli, Condoluci, Sacerdoti Coen. Strong Call-by-Value is Reasonable, Implosively. LICS 2021.
Accattoli, Dal Lago, Vanoni. The Space of Interaction. LICS 2021.
Accattoli, Faggian, Guerrieri. Factorize Factorization. CSL 2021.
Accattoli, Dal Lago, Vanoni. The Machinery of Interaction. PPDP 2020.
Accattoli, Díaz-Caro. Functional Pearl: the Distributive Lambda Calculus. FLOPS 2020.
Accattoli, Faggian, Guerrieri. Factorization and Normalization, Essentially. APLAS 2019.
Condoluci, Accattoli, Sacerdoti Coen. Sharing Equality is Linear. PPDP 2019.
Accattoli, Condoluci, Guerrieri, Sacerdoti Coen. Crumbling Abstract Machines. PPDP 2019.
Accattoli, Guerrieri, Leberle. Types by Need. ESOP 2019.
Alves, Kesner, Ventura. A Quantitative Understanding of Pattern Matching. TYPES 2019.
Accattoli, Guerrieri. Types of Fireballs. APLAS 2018.
Accattoli. Proof Nets and the Linear Substitution Calculus. ICTAC 2018.
Accattoli, Barras. The Negligible and Yet Subtle Cost of Pattern Matching. APLAS 2017.
Accattoli, Barras. Environments and the Complexity of Abstract Machines. PPDP 2017.
Accattoli, Guerrieri. Implementing Open Call-by-Value. FSEN 2017.
Invited papers:
Accattoli. A Fresh Look at the lambda Calculus. Invited paper at FSCD 2019. Slides of the invited talk.
Accattoli. (In)Efficiency and Reasonable Cost Models. Invited paper at LSFA 2017.