Skip to Main content Skip to Navigation

Incrementality and effect simulation in the simply typed lambda calculus

Lourdes del Carmen Gonzalez Huesca 1, 2 
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : Certified programming is a framework in which any program is correct by construction. Proof assistants and dependently typed programming languages are the representatives of this paradigm where the proof and implementation of a program are done at the same time. However, it has some limitations: a program in Type Theory is built only with pure and total functions. Our objective is to write efficient and certified programs. The contributions of this work are the formalization, in the Simply Typed Lambda Calculus, of two mechanisms to achieve efficiency: to validate impure computations and to optimize computations by incrementality. An impure computation, that is a program with effects, and its validation in a functional and total language is done through a posteriori simulation. The simulation is performed afterwards on a monadic procedure and is guided by a prophecy. An efficient oracle is responsible for producing prophecies which is actually, the monadic procedure itself translated into an effectful programming language. The second contribution is an optimization to perform incremental computations. Incrementality as a way to propagate an input change into a corresponding output change is guided by formal change descriptions over terms and dynamic differentiation of functions. Displaceable types represent data-changes while an extension of the simply typed lambda calculus with differentials and partial derivatives offers a language to reason about incrementality.
Document type :
Complete list of metadata

Cited literature [115 references]  Display  Hide  Download
Contributor : Lourdes del Carmen González Huesca Connect in order to contact the contributor
Submitted on : Monday, January 4, 2016 - 11:58:21 PM
Last modification on : Friday, January 21, 2022 - 3:22:27 AM
Long-term archiving on: : Thursday, April 7, 2016 - 4:47:23 PM


  • HAL Id : tel-01248531, version 1



Lourdes del Carmen Gonzalez Huesca. Incrementality and effect simulation in the simply typed lambda calculus. Computer Science [cs]. Universite Paris Diderot-Paris VII, 2015. English. ⟨tel-01248531⟩



Record views


Files downloads