Least and Greatest Fixed Points in Ludics

David Baelde 1, * Amina Doumane 2, 3 Alexis Saurin 2, 3
* Auteur correspondant
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 : Various logics have been introduced in order to reason over (co)inductive specifications and, through the Curry-Howard correspondence, to study computation over inductive and coinductive data. The logic µMALL is one of those logics, extending multiplicative and additive linear logic with least and greatest fixed point operators. In this paper, we investigate the semantics of µMALL proofs in (computational) ludics. This framework is built around the notion of design, which can be seen as an analogue of the strategies of game semantics. The infinitary nature of designs makes them particularly well suited for representing computations over infinite data. We provide µMALL with a denotational semantics, interpreting proofs by designs and formulas by particular sets of designs called behaviours. Then we prove a completeness result for the class of "essentially finite designs" , which are those designs performing a finite computation followed by a copycat. On the way to completeness, we establish decidability and completeness of semantic inclusion.
Type de document :
Pré-publication, Document de travail
This document corresponds to the long version of a paper accepted for publication at CSL 2015. 2015
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01178396
Contributeur : David Baelde <>
Soumis le : lundi 20 juillet 2015 - 16:32:53
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37
Document(s) archivé(s) le : mercredi 21 octobre 2015 - 17:11:17

Fichier

main.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

  • HAL Id : hal-01178396, version 1

Collections

Citation

David Baelde, Amina Doumane, Alexis Saurin. Least and Greatest Fixed Points in Ludics. This document corresponds to the long version of a paper accepted for publication at CSL 2015. 2015. 〈hal-01178396〉

Partager

Métriques

Consultations de la notice

400

Téléchargements de fichiers

119