Skip to Main content Skip to Navigation
Conference papers

Algebras and Coalgebras in the Light Affine Lambda Calculus

Abstract : Algebra and coalgebra are widely used to model data types in functional programming languages and proof assistants. Their use permits to better structure the computations and also to enhance the expressivity of a language or of a proof system. The use of algebras and coalgebras in proof assistants relies on the possibility of integrating them in strongly normalizing languages such as System F or the calculus of constructions without loosing the good logical properties of the calculus. In fact, in those systems it is possible to define weak (initial) algebras and weak (final) coalgebra by using parametric polymorphism. In this work we study the problem of defining algebras and coalgebra in Light Linear Logic, a system characterizing the complexity class P. Due to the stratified nature of Light Linear Logic, we need to consider stratified versions of (weak) algebras and coalgebras. Thanks to these notions we are able to define standard algebraic and coalgebraic data types in our language.
Document type :
Conference papers
Complete list of metadatas

Cited literature [38 references]  Display  Hide  Download
Contributor : Romain Péchoux <>
Submitted on : Friday, October 9, 2015 - 3:40:52 PM
Last modification on : Tuesday, December 8, 2020 - 9:47:05 AM
Long-term archiving on: : Sunday, January 10, 2016 - 10:12:37 AM


Files produced by the author(s)


  • HAL Id : hal-01112165, version 1



Marco Gaboardi, Romain Péchoux. Algebras and Coalgebras in the Light Affine Lambda Calculus. The 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), Aug 2015, Vancouver, Canada. ⟨hal-01112165⟩



Record views


Files downloads