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.
Type de document :
Communication dans un congrès
ACM. The 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), Aug 2015, Vancouver, Canada. 2015
Liste complète des métadonnées

Littérature citée [38 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01112165
Contributeur : Romain Péchoux <>
Soumis le : vendredi 9 octobre 2015 - 15:40:52
Dernière modification le : jeudi 11 janvier 2018 - 06:21:25
Document(s) archivé(s) le : dimanche 10 janvier 2016 - 10:12:37

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01112165, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

183

Téléchargements de fichiers

186