Group aces

aces (Autonomous Critical Embedded Systems)

LTCI, Telecom Paris

Themes: foundations of computer science; digital trust; next generation digital infrastructure

The research areas of the Autonomous Critical Embedded Systems team address concurrent systems, including parallel systems and distributed systems, for which non-operational properties such as performance and security need to be guaranteed.

Contact person: Laurent Pautet, https://perso.telecom-paristech.fr/pautet/

Web site: https://www.telecom-paris.fr/en/research/laboratories/information-processing-and-communication-laboratory-ltci/research-teams/autonomous-critical-embedded-systems

Journal articles

2022

ref_biblio: Sonia Marin, Dale Miller, Elaine Pimentel, Marco Volpe. From axioms to synthetic inference rules via focusing. Annals of Pure and Applied Logic, Elsevier Masson, 2022, 173 (5), pp.103091. ⟨10.1016/j.apal.2022.103091⟩. ⟨hal-03792129⟩
Accès au texte intégral et bibtex

2021

ref_biblio: Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni. The (In)Efficiency of interaction. Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (POPL), pp.1-33. ⟨10.1145/3434332⟩. ⟨hal-03346750⟩
Accès au texte intégral et bibtex

ref_biblio: Marianna Girlando, Sara Negri, Nicola Olivetti. Uniform labelled calculi for preferential conditional logics based on neighbourhood semantics. Journal of Logic and Computation, Oxford University Press (OUP), 2021, 31 (3), pp.947-997. ⟨10.1093/logcom/exab019⟩. ⟨hal-02330319v3⟩
Accès au texte intégral et bibtex

ref_biblio: Tomer Libal, Dale Miller. Functions-as-constructors higher-order unification: extended pattern unification. Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2021, ⟨10.1007/s10472-021-09774-y⟩. ⟨hal-03457303⟩
Accès au bibtex

ref_biblio: Sonia Marin, Marianela Morales, Lutz Strassburger. A fully labelled proof system for intuitionistic modal logics. Journal of Logic and Computation, Oxford University Press (OUP), 2021, 31 (3), pp.998-1022. ⟨10.1093/logcom/exab020⟩. ⟨hal-02390454v3⟩
Accès au texte intégral et bibtex

ref_biblio: Dale Miller, Alexandre Viel. The undecidability of proof search when equality is a logical connective. Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2021, ⟨10.1007/s10472-021-09764-0⟩. ⟨hal-03457312⟩
Accès au texte intégral et bibtex

ref_biblio: Dale Miller. Reciprocal Influences Between Proof Theory and Logic Programming. Philosophy & Technology, Springer, 2021, 34, pp.75-104. ⟨10.1007/s13347-019-00370-x⟩. ⟨hal-02368867⟩
Accès au texte intégral et bibtex

ref_biblio: Dale Miller. A Survey of the Proof-Theoretic Foundations of Logic Programming. Theory and Practice of Logic Programming, Cambridge University Press (CUP), 2021, pp.1-46. ⟨10.1017/S1471068421000533⟩. ⟨hal-03411144⟩
Accès au bibtex

ref_biblio: Alban Reynaud, Gabriel Scherer, Jeremy Yallop. A practical mode system for recursive definitions. Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (POPL), pp.1-29. ⟨10.1145/3434326⟩. ⟨hal-03125031⟩
Accès au texte intégral et bibtex

2020

ref_biblio: Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner. Tight typings and split bounds, fully developed. Journal of Functional Programming, Cambridge University Press (CUP), 2020, 30, ⟨10.1017/S095679682000012X⟩. ⟨hal-03089347⟩
Accès au bibtex

2019

ref_biblio: Noam Zeilberger. A sequent calculus for a semi-associative law. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2019, 15 (1), pp.1-23. ⟨10.23638/LMCS-15(1:9)2019⟩. ⟨hal-03131847⟩
Accès au bibtex

Conference papers

2022

ref_biblio: Nicolas Chataing, Camille Noûs, Gabriel Scherer. Déboîter les constructeurs. Journées Francophones des Langages Applicatifs, Feb 2022, Saint-Médard-d'Excideuil, France. ⟨hal-03510931⟩
Accès au texte intégral et bibtex

ref_biblio: Pablo Donato, Pierre-Yves Strub, Benjamin Werner. Actema : une interface graphique et gestuelle pour preuves formelles (démonstration). 33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.267-268. ⟨hal-03626854⟩
Accès au texte intégral et bibtex

ref_biblio: Willem Heijltjes, Dominic Hughes, Lutz Strassburger. Normalization Without Syntax. FSCD 2022, Aug 2022, Haifa, Israel. ⟨hal-03654060⟩
Accès au texte intégral et bibtex

ref_biblio: Paul-André Melliès, Noam Zeilberger. Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem. MFPS 2022 - 38th conference on Mathematical Foundations for Programming Semantics, Jul 2022, Ithaca, NY, United States. ⟨hal-03702762⟩
Accès au texte intégral et bibtex

2021

ref_biblio: Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri. Factorize Factorization. CSL 2021 - 29th EACSL Annual Conference on Computer Science Logic, Jan 2021, Ljubljana, Slovenia. ⟨10.4230/LIPIcs.CSL.2021.22⟩. ⟨hal-03044338⟩
Accès au texte intégral et bibtex

ref_biblio: Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni. The Space of Interaction. LICS 2021 - 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2021, Rome, France. pp.1-13, ⟨10.1109/LICS52264.2021.9470726⟩. ⟨hal-03346767⟩
Accès au texte intégral et bibtex

ref_biblio: Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen. Strong Call-by-Value is Reasonable, Implosively. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, Italy. pp.1-14, ⟨10.1109/LICS52264.2021.9470630⟩. ⟨hal-03475461⟩
Accès au bibtex

ref_biblio: Frédéric Bour, Basile Clément, Gabriel Scherer. Tail Modulo Cons. JFLA 2021 - Journées Francophones des Langages Applicatifs, Apr 2021, Saint Médard d’Excideuil, France. ⟨hal-03146495⟩
Accès au texte intégral et bibtex

ref_biblio: Nicolas Chataing, Gabriel Scherer. Unfolding ML datatype declarations without loops. ML Family Workshop, Aug 2021, online, South Korea. ⟨hal-03510898⟩
Accès au texte intégral et bibtex

ref_biblio: Kaustuv Chaudhuri. Subformula Linking for Intuitionistic Logic with Application to Type Theory. CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA (Virtual), United States. pp.200-216, ⟨10.1007/978-3-030-79876-5_12⟩. ⟨hal-03528659⟩
Accès au texte intégral et bibtex

ref_biblio: Olivier Martinot, Gabriel Scherer. Frozen inference constraints for type-directed disambiguation. ML Family Workshop, Aug 2021, online, South Korea. ⟨hal-03510890⟩
Accès au texte intégral et bibtex

ref_biblio: Wendlasida Ouedraogo, Danko Ilik, Lutz Strassburger. Demo Paper: Coqlex, an approach to generate verified lexers. ML 2021-ACM SIGPLAN Workshop on ML, Aug 2021, Online event, United States. ⟨hal-03470713⟩
Accès au texte intégral et bibtex

ref_biblio: Lutz Strassburger, Dominic J D Hughes, Jui-Hsuan Wu. Combinatorial Proofs and Decomposition Theorems for First-order Logic. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, Italy. pp.1-13, ⟨10.1109/LICS52264.2021.9470579⟩. ⟨hal-03369764⟩
Accès au texte intégral et bibtex

2020

ref_biblio: Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni. The Machinery of Interaction. PPDP '20 - 22nd International Symposium on Principles and Practice of Declarative Programming, Sep 2020, Bologna, Italy. pp.1-15, ⟨10.1145/3414080.3414108⟩. ⟨hal-03089342⟩
Accès au bibtex

ref_biblio: Beniamino Accattoli, Alejandro Díaz-Caro. Functional Pearl: The Distributive $\lambda$-Calculus. FLOPS 2020 - 15th International Symposium on Functional and Logic Programming, Sep 2020, Akita, Japan. pp.33-49, ⟨10.1007/978-3-030-59025-3_3⟩. ⟨hal-03089254⟩
Accès au bibtex

ref_biblio: Matteo Acclavio, Ross Horne, Lutz Strassburger. Logic beyond formulas: a proof system on graphs. LICS 2020 - 35th ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken, Germany. pp.38-52, ⟨10.1145/3373718.3394763⟩. ⟨hal-02560105⟩
Accès au texte intégral et bibtex

ref_biblio: Matteo Acclavio, Roberto Maieli. Generalized connectives for multiplicative linear logic. CSL 2020 - 28th EACSL annual conference on Computer Science Logic, Jan 2020, Barcelona, Spain. pp.6:1-6:15, ⟨10.4230/LIPIcs.CSL.2020.6⟩. ⟨hal-02492258⟩
Accès au texte intégral et bibtex

ref_biblio: Nicolas Blanco, Noam Zeilberger. Bifibrations of Polycategories and Classical Linear Logic. MFPS 2020 - 36th Conference on Mathematical Foundations of Programming Semantics, Jun 2020, Paris, France. pp.29-52, ⟨10.1016/j.entcs.2020.09.003⟩. ⟨hal-03031058⟩
Accès au bibtex

ref_biblio: Davide Catta, Luc Pellissier, Christian Retoré. Inferential Semantics as Argumentative Dialogues. DCAI 2020 - 17th International Conference on Distributed Computing and Artificial Intelligence, Jun 2020, L´Aquila, Italy. pp.72-81, ⟨10.1007/978-3-030-53829-3_7⟩. ⟨hal-02922646⟩
Accès au texte intégral et bibtex

ref_biblio: Matteo Cimini, Dale Miller, Jeremy G Siek. Extrinsically Typed Operational Semantics for Functional Languages. SLE 2020 - 13th ACM SIGPLAN/International Conference on Software Language Engineering, Nov 2020, Virtual, United States. ⟨hal-03007256⟩
Accès au texte intégral et bibtex

ref_biblio: Marianna Girlando, Lutz Strassburger. MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description). IJCAR 2020 - 10th International Joint Conference, Jul 2020, Paris, France. pp.398-407, ⟨10.1007/978-3-030-51054-1_25⟩. ⟨hal-02457240v3⟩
Accès au texte intégral et bibtex

ref_biblio: Marianna Girlando, Bjoern Lellmann, Nicola Olivetti, Stefano Pesce, Gian Luca Pozzato. Theorem proving for Lewis Logics of Counterfactual Reasoning. CILC 2020 - 35th Edition of the Italian Conference on Computational Logic, Oct 2020, Rende / Virtual, Italy. ⟨hal-03080670⟩
Accès au texte intégral et bibtex

ref_biblio: Sonia Marin, Marianela Morales. Fully structured proof theory for intuitionistic modal logics. AiML 2020 - Advances in Modal Logic, Aug 2020, Helsinki, Finland. ⟨hal-03048959⟩
Accès au texte intégral et bibtex

ref_biblio: Olivier Martinot, Gabriel Scherer. Quantified Applicatives: API design for type-inference constraints. ML Family Workshop, Aug 2020, Jersey City / Online, United States. ⟨hal-03145040⟩
Accès au texte intégral et bibtex

ref_biblio: Francesco Mecca, Gabriel Scherer. Translation validation of a pattern-matching compiler. ML Family Workshop, Aug 2020, New Jersey /Online, United States. ⟨hal-03145030⟩
Accès au texte intégral et bibtex

ref_biblio: Dale Miller. A Distributed and Trusted Web of Formal Proofs. ICDCIT 2020 - 16th International Conference on Distributed Computing and Internet Technology, Jan 2020, Bhubaneswar, India. pp.21-40, ⟨10.1007/978-3-030-36987-3_2⟩. ⟨hal-02468229⟩
Accès au texte intégral et bibtex

ref_biblio: Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. Deductive systems and coherence for skew prounital closed categories. LFMTP 2020 - 15th International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, Jun 2020, Paris, France. pp.35-53, ⟨10.4204/eptcs.332.3⟩. ⟨hal-03031107⟩
Accès au bibtex

ref_biblio: Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. Eilenberg-Kelly Reloaded. MFPS 2020 - 36th Conf. on Mathematical Foundations of Programming Semantics, Jun 2020, Paris, France. pp.233-256, ⟨10.1016/j.entcs.2020.09.012⟩. ⟨hal-03031068⟩
Accès au bibtex

ref_biblio: Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. Proof theory of partially normal skew monoidal categories. ACT 2020 - 3rd Applied Category Theory Conference, Jul 2020, Cambridge, MA, United States. pp.230-246, ⟨10.4204/eptcs.333.16⟩. ⟨hal-03031087⟩
Accès au bibtex

2018

ref_biblio: Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. The Sequent Calculus of Skew Monoidal Categories. Proc. of 34th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXIV, Jun 2018, Halifax, Canada. pp.345-370, ⟨10.1016/j.entcs.2018.11.017⟩. ⟨hal-03031126⟩
Accès au bibtex

ref_biblio: Noam Zeilberger. A theory of linear typings as flows on 3-valent graphs. LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford United Kingdom, France. pp.919-928, ⟨10.1145/3209108.3209121⟩. ⟨hal-03132231⟩
Accès au bibtex

Book sections

2021

ref_biblio: Matteo Acclavio, Davide Catta, Lutz Strassburger. Game Semantics for Constructive Modal Logic. Automated Reasoning with Analytic Tableaux and Related Methods, 12842, Springer International Publishing, pp.428-445, 2021, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-86059-2_25⟩. ⟨hal-03369819⟩
Accès au texte intégral et bibtex

2020

ref_biblio: Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. The sequent calculus of skew monoidal categories (extended version). C. Casadio; P. J. Scott. Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, Springer, In press, Outstanding Contributions to Logic. ⟨hal-03031139⟩
Accès au bibtex

Lectures

2021

ref_biblio: Willem Heijltjes, Lutz Strassburger. From Proof Nets to Combinatorial Proofs - A New Approach to Hilbert's 24th Problem. École thématique. From Proof Nets to Combinatorial Proofs - A New Approach to Hilbert's 24th Problem, Utrecht / Virtual, Netherlands. 2021. ⟨hal-03316571⟩
Accès au texte intégral et bibtex

Reports

2020

ref_biblio: Roberto Blanco, Matteo Manighetti, Dale Miller. FPC-Coq: Using ELPI to elaborate external proof evidence into Coq proofs. [Research Report] Inria Saclay. 2020. ⟨hal-02974002⟩
Accès au texte intégral et bibtex

Preprints, Working Papers, ...

2022

ref_biblio: Matteo Manighetti, Dale Miller. Computational logic based on linear logic and fixed points. 2022. ⟨hal-03579451⟩
Accès au texte intégral et bibtex

2021

ref_biblio: Matteo Acclavio, Davide Catta, Lutz Strassburger. Towards a Denotational Semantics for Proofs in Constructive Modal Logic. 2021. ⟨hal-03201439⟩
Accès au texte intégral et bibtex

ref_biblio: Olivier Bodini, Alexandros Singh, Noam Zeilberger. Asymptotic Distribution of Parameters in Trivalent Maps and Linear Lambda Terms. 2021. ⟨hal-03495894⟩
Accès au bibtex

ref_biblio: Chuck Liang, Dale Miller. Focusing Gentzen's LK proof system. 2021. ⟨hal-03457379⟩
Accès au texte intégral et bibtex

2020

ref_biblio: Matteo Acclavio, Ross Horne, Lutz Strassburger. An Analytic Propositional Proof System On Graphs. 2020. ⟨hal-03087392⟩
Accès au texte intégral et bibtex

ref_biblio: Marianna Girlando, Marianela Morales. MOILab: towards a labelled theorem prover for intuitionistic modal logics. 2020. ⟨hal-03048966⟩
Accès au texte intégral et bibtex