Classical realizability and arithmetical formulæ. - Mauricio Guillermo; Étienne Miquey (Math. Struct. Comput. Sci., 2017)

Classical realizability and side-effects. (Réalisabilité classique et effets de bords). - Étienne Miquey (2017)

Realizability Interpretation and Normalization of Typed Call-by-Need lambda -calculus with Control. - Étienne Miquey; Hugo Herbelin (FoSSaCS, 2018)

Formalizing Implicative Algebras in Coq. - Étienne Miquey (ITP, 2018)

A sequent calculus with dependent types for classical arithmetic. - Étienne Miquey (LICS, 2018)

Realizability Interpretation and Normalization of Typed Call-by-Need λ-calculus With Control. - Étienne Miquey; Hugo Herbelin (CoRR, 2018)

A constructive proof of dependent choice in classical arithmetic via memoization. - Étienne Miquey (CoRR, 2019)

A Classical Sequent Calculus with Dependent Types. - Étienne Miquey (ACM Trans. Program. Lang. Syst., 2019)

Revisiting the Duality of Computation: An Algebraic Analysis of Classical Realizability Models. - Étienne Miquey (CSL, 2020)

A calculus of expandable stores: Continuation-and-environment-passing style translations. - Hugo Herbelin; Étienne Miquey (LICS, 2020)

Realizability with Stateful Computations for Nonstandard Analysis. - Bruno Dinis; Étienne Miquey (CSL, 2021)

Evidenced Frames: A Unifying Framework Broadening Realizability Models. - Liron Cohen 001; Étienne Miquey; Ross Tate (LICS, 2021)

Concurrent Realizability on Conjunctive Structures. - Emmanuel Beffara; Félix Castro; Mauricio Guillermo; Étienne Miquey (FSCD, 2023)

Stateful Realizers for Nonstandard Analysis. - Bruno Dinis; Étienne Miquey (Log. Methods Comput. Sci., 2023)

From Partial to Monadic: Combinatory Algebra with Effects. - Liron Cohen 001; Ariel Grunfeld; Dominik Kirst; Étienne Miquey (FSCD, 2025)

Syntactic Effectful Realizability in Higher-Order Logic. - Liron Cohen 001; Ariel Grunfeld; Dominik Kirst; Étienne Miquey (CoRR, 2025)