A preview of a tutorial on L (polarized μμ-tilde)

Kenji Maillard 1 Étienne Miquey 2, 3 Xavier Montillet 2, 3 Guillaume Munch-Maccagnoni 3, 2 Gabriel Scherer 4
1 PROSECCO - Programming securely with cryptography
Inria de Paris
2 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
3 LS2N - Laboratoire des Sciences du Numérique de Nantes
4 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : We are working on a new tutorial presentation of L, the polarized version of Curien-Herbelin’s μμ̃ -calculus. The calculus μμ̃ was introduced in Curien and Herbelin [2000] as a good term calculus for classical logic, which in particular reveals a perfect symmetry (in the classical setting) between call-by-value and call-by-name evaluation. Its polarized version, L, restricts the reduction rules according to a type- or polarity-based evaluation order; as Call-By-Push-Value [Levy 1999], it can express and mix both call-by-name and call-by-value terms in the same program, and is an interesting vehicle to study side-effects. We would like to offer a presentation of a fragment of our in-progress tutorial to the HOPE audience, as an act of popularization for newcomers, and as the best way to get feedback on our approach from newcomers and experts alike.
Type de document :
Communication dans un congrès
HOPE 2018 - 7th ACM SIGPLAN Workshop on Higher-Order Programming with Effects, Sep 2018, St. Louis, United States
Liste complète des métadonnées
https://hal.inria.fr/hal-01992294
Contributeur : Guillaume Munch-Maccagnoni <>
Soumis le : jeudi 24 janvier 2019 - 13:09:48
Dernière modification le : mardi 29 janvier 2019 - 13:52:57

Identifiants

  • HAL Id : hal-01992294, version 1

Collections

INRIA-ROCQ | LIX | UNAM | X-LIX | X | LS2N | INRIA | UNIV-NANTES | X-DEP-INFO | PARISTECH | LS2N-GALLINETTE | UNIV-PARIS-SACLAY

Citation

Kenji Maillard, Étienne Miquey, Xavier Montillet, Guillaume Munch-Maccagnoni, Gabriel Scherer. A preview of a tutorial on L (polarized μμ-tilde). HOPE 2018 - 7th ACM SIGPLAN Workshop on Higher-Order Programming with Effects, Sep 2018, St. Louis, United States. 〈hal-01992294〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

64

Contact


archive-ouverte@inria.fr