Publications

Publications HAL de Sergueï Lenglet

Journal articles

titre
HOπ in Coq
auteur
Guillaume Ambal, Sergueï Lenglet, Alan Schmitt
article
Journal of Automated Reasoning, 2020, ⟨10.1007/s10817-020-09553-0⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02536463/file/jar.pdf BibTex
titre
Bisimulations for Delimited-Control Operators
auteur
Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
article
Logical Methods in Computer Science, 2019, 15 (2), pp.18:1-18:57. ⟨10.23638/LMCS-15(2:18)2019⟩
Accès au bibtex
https://arxiv.org/pdf/1804.08373 BibTex
titre
Proving Soundness of Extensional Normal-Form Bisimilarities
auteur
Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
article
Logical Methods in Computer Science, 2019, 15 (1), pp.31:1-31:24. ⟨10.23638/LMCS-15(1:31)2019⟩
Accès au bibtex
https://arxiv.org/pdf/1711.00113 BibTex
titre
Faithful (Meta-)Encodings Of Programmable Strategies Into Term Rewriting Systems
auteur
Horatiu Cirstea, Sergueï Lenglet, Pierre-Etienne Moreau
article
Logical Methods in Computer Science, 2017, 13 (4), pp.1-54. ⟨10.23638/LMCS-13(4:16)2017⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01479030/file/1705.08632v2.pdf BibTex
titre
Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation
auteur
Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
article
Logical Methods in Computer Science, 2017, 13 (3), ⟨10.23638/LMCS-13(3:27)2017⟩
Accès au bibtex
https://arxiv.org/pdf/1611.09626v5 BibTex
titre
Characterizing contextual equivalence in calculi with passivation
auteur
Sergueï Lenglet, Alan Schmitt, Jean-Bernard Stefani
article
Information and Computation, 2011, 209 (11), pp.1390-1433. ⟨10.1016/j.ic.2011.08.002⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00903877/file/journal.pdf BibTex

Conference papers

titre
Certified Derivation of Small-Step From Big-Step Skeletal Semantics
auteur
Guillaume Ambal, Sergueï Lenglet, Alan Schmitt, Camille Noûs
article
PPDP 2022 – 24th International Symposium on Principles and Practice of Declarative Programming, Sep 2022, Tbilisi, Georgia. pp.1-48, ⟨10.1145/3551357.3551384⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03768820/file/ppdp.pdf BibTex
titre
Non-Deterministic Abstract Machines
auteur
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Alan Schmitt
article
CONCUR 2022 – 33rd International Conference
 on Concurrency Theory, Sep 2022, Varsovie, Poland. pp.1-24, ⟨10.4230/LIPIcs.CONCUR.2022.7⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03772712/file/LIPIcs-CONCUR-2022-7.pdf BibTex
titre
Certified Abstract Machines for Skeletal Semantics
auteur
Guillaume Ambal, Sergueï Lenglet, Alan Schmitt
article
CPP 2022 – 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2022, Philadelphia, United States. pp.1-13, ⟨10.1145/3497775.3503676⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03466807/file/cpp.pdf BibTex
titre
A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers
auteur
Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
article
Formal Structures for Computation and Deduction, Jun 2020, Paris, France. ⟨10.4230/LIPIcs.FSCD.2020.7⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02559253/file/fscd.pdf BibTex
titre
Diacritical Companions
auteur
Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
article
MFPS 2019-Mathematical Foundations of Programming Semantics XXXV, Jun 2019, London, United Kingdom. ⟨10.1016/j.entcs.2019.09.003⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02136002/file/companion.pdf BibTex
titre
A Complete Normal-Form Bisimilarity for State
auteur
Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
article
FoSSaCS, Apr 2019, Prague, Czech Republic. ⟨10.1007/978-3-030-17127-8_6⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02086532/file/final.pdf BibTex
titre
HOπ in Coq
auteur
Sergueï Lenglet, Alan Schmitt
article
CPP 2018 – The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. pp.14, ⟨10.1145/3167083⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01614987/file/cpp18.pdf BibTex
titre
Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines
auteur
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, Alan Schmitt
article
LICS 2017 – 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. ⟨10.1109/LICS.2017.8005118⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01479035/file/lics.pdf BibTex
titre
Proving Soundness of Extensional Normal-Form Bisimilarities
auteur
Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
article
Mathematical Foundations of Programming Semantics XXXIII, Jun 2017, Ljubljana, Slovenia. ⟨10.1016/j.entcs.2018.03.015⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01650000/file/mfps.pdf BibTex
titre
Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation
auteur
Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
article
1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Jun 2016, Porto, Portugal. ⟨10.4230/LIPIcs.FSCD.2016.9⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01335959/file/LIPIcs-FSCD-2016-9.pdf BibTex
titre
Howe’s Method for Contextual Semantics
auteur
Sergueï Lenglet, Alan Schmitt
article
CONCUR 2015 26th International Conference on Concurrency Theory, Sep 2015, Madrid, Spain. ⟨10.4230/LIPIcs.CONCUR.2015.212⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01192699/file/Concur%2015.pdf BibTex
titre
A faithful encoding of programmable strategies into term rewriting systems
auteur
Horatiu Cirstea, Sergueï Lenglet, Pierre-Etienne Moreau
article
Rewriting Techniques and Application 2015, Jun 2015, Warsaw, Poland. pp.15, ⟨10.4230/LIPIcs.RTA.2015.74⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01168956/file/10.pdf BibTex
titre
Applicative Bisimilarities for Call-by-Name and Call-by-Value λμ-Calculus
auteur
Dariusz Biernacki, Sergueï Lenglet
article
Mathematical Foundations of Programming Semantics Thirtieth Conference, Jun 2014, Ithaca, United States. pp.49 – 64, ⟨10.1016/j.entcs.2014.10.004⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01080960/file/lambdamuentcs.pdf BibTex
titre
Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation
auteur
Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, Luca Padovani
article
POPL ’14, 41th ACM Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States. pp.5-17, ⟨10.1145/2535838.2535840⟩
Accès au bibtex
BibTex
titre
Environmental Bisimulations for Delimited-Control Operators
auteur
Dariusz Biernacki, Sergueï Lenglet
article
APLAS – 11th Asian Symposium on Programming Languages and Systems – 2013, Dec 2013, Melbourne, Australia. pp.333-348
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00903839/file/aplas.pdf BibTex
titre
Proving termination of evaluation for System F with control operators
auteur
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Marek Materzok
article
COS 2013 – First Workshop on Control Operators and their Semantics, Jun 2013, Eindhoven, Netherlands. pp.15-29, ⟨10.4204/EPTCS.127.2⟩
Accès au bibtex
https://arxiv.org/pdf/1309.1261 BibTex
titre
Normal Form Bisimulations for Delimited-Control Operators
auteur
Dariusz Biernacki, Sergueï Lenglet
article
Symposium on Functional and Logic Programming (FLOPS 2012), Jun 2012, Kobé, Japan. pp.47 – 61, ⟨10.1007/978-3-642-29822-6_7⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01399951/file/biernacki-lenglet-flops12.pdf BibTex
titre
Applicative Bisimulations for Delimited-Control Operators
auteur
Dariusz Biernacki, Sergueï Lenglet
article
Foundations of Software Science and Computation Structures (FoSSaCS 2012), Mar 2012, Tallinn, Estonia. pp.119 – 134, ⟨10.1007/978-3-642-28729-9_8⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01399945/file/biernacki-lenglet-fossacs12.pdf BibTex
titre
Expansion for Universal Quantifiers
auteur
Sergueï Lenglet, J B Wells
article
European Symposium On Programming (ESOP 2012), Mar 2012, Tallinn, Estonia. pp.456 – 475, ⟨10.1007/978-3-642-28869-2_23⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01405792/file/etaps_final.pdf BibTex
titre
Typing control operators in the CPS hierarchy
auteur
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet
article
PPDP – Principles and Practice of Declarative Programming, Jul 2011, Odense, Denmark. pp.149-160, ⟨10.1145/2003476.2003498⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00903834/file/hierarchy.pdf BibTex
titre
Howe’s Method for Calculi with Passivation
auteur
Sergueï Lenglet, Alan Schmitt, Jean-Bernard Stefani
article
20th International Conference on Concurrency Theory (CONCUR 2009), Sep 2009, Bologna, Italy. pp.448–462
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00486800/file/Lenglet2009Howes-Method-for-Cal.pdf BibTex
titre
Normal bisimulations in process calculi with passivation
auteur
Sergueï Lenglet, Alan Schmitt, Jean-Bernard Stefani
article
12th International Conference on Foundations of Software Science and Computational Structures (FOSSACS 2009), Mar 2009, York, United Kingdom. pp.257–271, ⟨10.1007/978-3-642-00596-1_19⟩
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00490810/file/2009.03.01-Eart-Normal_bisimulations_in_process_calculi_with_passivation_by_Lenglet._S_Schmitt._A_Stefani._J.pdf BibTex
titre
A Core Calculus for Scala Type Checking
auteur
Vincent Cremet, François Garillot, Sergueï Lenglet, Martin Odersky
article
Mathematical Foundations of Computer Science 2006, Aug 2006, Stará Lesná, Slovakia. pp.1-23, ⟨10.1007/11821069_1⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00903812/file/06-Cremet.pdf BibTex

Reports

titre
Non-Deterministic Abstract Machines
auteur
Małgorzata Biernacka, Dariusz Biernacki, Serguei Lenglet, Alan Schmitt
article
[Research Report] RR-9475, Inria. 2022, pp.1-33
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03545768/file/RR-9475.pdf BibTex
titre
Automatic Transformation of a Big-Step Skeletal Semantics into Small-Step
auteur
Guillaume Ambal, Alan Schmitt, Sergueï Lenglet
article
[Research Report] RR-9363, Inria Rennes – Bretagne Atlantique. 2020
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02946930/file/RR-9363.pdf BibTex
titre
A Complete Normal-Form Bisimilarity for State
auteur
Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
article
[Research Report] RR-9251, Inria Nancy – Grand Est. 2019
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02002115/file/RR-9251.pdf BibTex
titre
Bisimulations for Delimited-Control Operators
auteur
Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
article
[Research Report] RR-9096, Inria Nancy – Grand Est. 2017
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01207112/file/RR-9096.pdf BibTex
titre
Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines
auteur
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, Alan Schmitt
article
[Research Report] RR-9052, Inria. 2017
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01507625/file/RR-9052.pdf BibTex
titre
Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation
auteur
Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
article
[Research Report] RR-8905, Inria. 2016
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01305137/file/RR-8905v2.pdf BibTex
titre
Howe’s Method for Contextual Semantics
auteur
Sergueï Lenglet, Alan Schmitt
article
[Research Report] RR-8750, Inria. 2015, pp.31
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01168865/file/RR-8750.pdf BibTex
titre
Sound and Complete Bisimilarities for Call-by-Name and Call-by-Value Lambda-mu Calculus
auteur
Dariusz Biernacki, Sergueï Lenglet
article
[Research Report] RR-8447, INRIA. 2014
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00926100/file/RR-8447.pdf BibTex
titre
Howe’s Method for Early Bisimilarities
auteur
Sergueï Lenglet, Alan Schmitt, Jean-Bernard Stefani
article
[Research Report] RR-6773, INRIA. 2008, pp.69
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00347137/file/RR-6773v2.pdf BibTex
titre
Normal bisimulations in process calculi with passivation
auteur
Sergueï Lenglet, Alan Schmitt, Jean-Bernard Stefani
article
[Research Report] RR-6664, INRIA. 2008, pp.102
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00330565/file/RR-6664.pdf BibTex
titre
A practical type system for generalized recursion
auteur
Tom Hirschowitz, Serguei Lenglet
article
[Research Report] Laboratoire de l’informatique du parallélisme. 2005, 2+50p
Accès au texte intégral et bibtex
https://hal-lara.archives-ouvertes.fr/hal-02102506/file/RR2005-22.pdf BibTex

Theses

titre
Bisimulations dans les calculs avec passivation
auteur
Sergueï Lenglet
article
Informatique [cs]. Université Joseph-Fourier – Grenoble I, 2010. Français. ⟨NNT : ⟩
Accès au texte intégral et bibtex
https://theses.hal.science/tel-00447857/file/these.pdf BibTex

Preprints, Working Papers, …

titre
Leaf-First Zipper Semantics
auteur
Sergueï Lenglet, Alan Schmitt
article
2024
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04537440/file/RR-9546.pdf BibTex
titre
A faithful encoding of programmable strategies into term rewriting systems
auteur
Horatiu Cirstea, Sergueï Lenglet, Pierre-Etienne Moreau
article
2015
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01119941/file/paper.pdf BibTex
titre
Environmental Bisimulations for Delimited-Control Operators
auteur
Dariusz Biernacki, Sergueï Lenglet
article
2013
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00862189/file/aplasLong.pdf BibTex
titre
Applicative Bisimulations for Delimited-Control Operators
auteur
Dariusz Biernacki, Sergueï Lenglet
article
2012
Accès au bibtex
https://arxiv.org/pdf/1201.0874 BibTex