Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

22 résultats
Image document

Do CPS translations also translate realizers?

Samuel Gardelle , Étienne Miquey
JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.134-151
Communication dans un congrès hal-03910311v2
Image document

Revisiting the duality of computation: an algebraic analysis of classical realizability models

Étienne Miquey
CSL 2020 - Conference on Computer Science Logic, Jan 2020, Barcelone, Spain. pp.1-52, ⟨10.4230/LIPIcs.CSL.2020.30⟩
Communication dans un congrès hal-02305560v2
Image document

Formalizing Implicative Algebras in Coq

Étienne Miquey
ITP 2018 - 9th International Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. pp.459-476, ⟨10.1007/978-3-319-94821-8_27⟩
Communication dans un congrès hal-01703524v1
Image document

A Classical Sequent Calculus with Dependent Types

Étienne Miquey
ACM Transactions on Programming Languages and Systems (TOPLAS), 2019, 41 (2), pp.1-48. ⟨10.1145/3230625⟩
Article dans une revue hal-01519929v3
Image document

Classical realizability and side-effects

Étienne Miquey
Logic in Computer Science [cs.LO]. Université Sorbonne Paris Cité - Université Paris Diderot (Paris 7); Universidad de la República - Montevideo, Uruguay, 2017. English. ⟨NNT : ⟩
Thèse tel-01653733v2
Image document

Continuation-and-environment-passing style translations: a focus on call-by-need

Hugo Herbelin , Étienne Miquey
2019
Pré-publication, Document de travail hal-01972846v1
Image document

A continuation-passing-style interpretation of simply-typed call-by-need λ-calculus with control within System F

Hugo Herbelin , Étienne Miquey
CL&C'16. Sixth International Workshop on. Classical Logic and Computation, Jun 2016, Porto, Portugal
Communication dans un congrès hal-01302696v2
Image document

A sequent calculus with dependent types for classical arithmetic

Étienne Miquey
LICS 2018 - 33th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford, United Kingdom. pp.720-729, ⟨10.1145/3209108.3209199⟩
Communication dans un congrès hal-01703526v2
Image document

Realizability with stateful computations for nonstandard analysis

Bruno Dinis , Étienne Miquey
CSL 2021 - Computer Science Logic, Jan 2021, Ljubljana, Slovenia
Communication dans un congrès hal-03002239v1
Image document

Concurrent Realizability on Conjunctive Structures

Emmanuel Beffara , Félix Castro , Mauricio Guillermo , Étienne Miquey
FSCD 2023 - 8th International Conference on Formal Structures for Computation and Deduction, Jul 2023, Rome, Italy
Communication dans un congrès hal-04083002v2
Image document

Dependent Type Theory in Polarised Sequent Calculus (abstract)

Étienne Miquey , Xavier Montillet , Guillaume Munch-Maccagnoni
TYPES 2020 - 26th International Conference on Types for Proofs and Programs, Mar 2020, Torino, Italy. pp.1-3
Communication dans un congrès hal-02505671v1
Image document

Stateful Realizers for Nonstandard Analysis

Bruno Dinis , Étienne Miquey
Logical Methods in Computer Science, 2023, Volume 19, Issue 2, ⟨10.46298/LMCS-19(2:7)2023⟩
Article dans une revue hal-04053612v1
Image document

Realizability games for arithmetical formulæ

Étienne Miquey
Worskshop GaLoP2015, Apr 2015, Londres, United Kingdom
Communication dans un congrès hal-01248093v1
Image document

A Classical Sequent Calculus with Dependent Types

Étienne Miquey
26th European Symposium on Programming, Apr 2017, Uppsala, Sweden
Communication dans un congrès hal-01375977v3
Image document

Normalization and continuation-passing-style interpretation of simply-typed call-by-need λ-calculus with control

Hugo Herbelin , Étienne Miquey
2017
Pré-publication, Document de travail hal-01570987v1
Image document

Realizability Interpretation and Normalization of Typed Call-by-Need λ-calculus With Control

Étienne Miquey , Hugo Herbelin
FOSSACS 18 - 21st International Conference on Foundations of Software Science and Computation Structures, Apr 2018, Thessalonique, Greece. pp.276-292, ⟨10.1007/978-3-319-89366-2_15⟩
Communication dans un congrès hal-01624839v2
Image document

A calculus of expandable stores

Hugo Herbelin , Étienne Miquey
LICS 2020 - 35th ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken / Virtual, Germany. pp.564-577, ⟨10.1145/3373718.3394792⟩
Communication dans un congrès hal-02557823v2
Image document

A Classical Sequent Calculus with Dependent Types

Étienne Miquey
2018
Pré-publication, Document de travail hal-01744359v1
Image document

Evidenced Frames: A Unifying Framework Broadening Realizability Models

Liron Cohen , Étienne Miquey , Ross Tate
LICS 2021, Jul 2021, Rome, Italy
Communication dans un congrès hal-03422961v1
Image document

Classical realizability and arithmetical formulæ

Mauricio Guillermo , Étienne Miquey
Mathematical Structures in Computer Science, 2016, ⟨10.1017/S0960129515000559⟩
Article dans une revue hal-01247989v1

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

Kenji Maillard , Étienne Miquey , Xavier Montillet , Guillaume Munch-Maccagnoni , Gabriel Scherer
HOPE 2018 - 7th ACM SIGPLAN Workshop on Higher-Order Programming with Effects, Sep 2018, St. Louis, United States
Communication dans un congrès hal-01992294v1
Image document

Toward dependent choice: a classical sequent calculus with dependent types

Hugo Herbelin , Étienne Miquey
TYPES 2015, May 2015, Tallinn, Estonia
Communication dans un congrès hal-01247998v1