Skip to Main content Skip to Navigation

hal-03455968v1  Conference papers
Paul-André Melliès. Asynchronous Template Games and the Gray Tensor Product of 2-Categories
LICS 2021 - 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2021, Rome, Italy. ⟨10.1109/LICS52264.2021.9470758⟩
hal-03320556v1  Conference papers
Théo ZimmermannJean-Rémy Falleri. A grounded theory of Community Package Maintenance Organizations-Registered Report
ICSME 2021 - 37th International Conference on Software Maintenance and Evolution, Sep 2021, Luxembourg City / Virtual, Luxembourg
hal-02173207v1  Conference papers
Rémi NolletAlexis SaurinChristine Tasson. PSPACE-Completeness of a Thread Criterion for Cyclic Proofs in Linear Logic with Least and Greatest Fixed Points
TABLEAUX 2019 - 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2019, London, United Kingdom. ⟨10.1007/978-3-030-29026-9_18⟩
hal-03210222v1  Conference papers
Lucas Massoni SguerraPierre JouvelotEmilio Jesús Gallego AriasGérard MemmiFabien Coelho. Blockchain Performance Benchmarking: a VCG Auction Smart Contract Use Case for Ethereum and Tezos (Short Paper)
FAB 2021 - Fourth International Symposium on Foundations and Applications of Blockchain, University of California, Davis, May 2021, Davis / Virtual, United States
hal-02534965v2  Conference papers
Théo Zimmermann. A first look at an emerging model of community organizations for the long-term maintenance of ecosystems' packages
SoHeal 2020 - 3rd International Workshop on Software Health, May 2020, Seoul / Virtual, South Korea. ⟨10.1145/3387940.3392209⟩
hal-03404668v2  Conference papers
Pierre CastéranJérémy DamourKarl PalmskogClément Pit-ClaudelThéo Zimmermann. Hydras & Co.: Formalized mathematics in Coq for inspiration and entertainment
Journées Francophones des Langages Applicatifs: JFLA 2022, Feb 2022, St-Médard d'Excideuil, France
hal-02422273v1  Conference papers
Thomas LetanYann Régis-Gianas. FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
CPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2020, Nouvelle-Orléans, United States. pp.1-15, ⟨10.1145/3372885.3373812⟩
hal-03322174v1  Conference papers
Emilio Jesús Gallego AriasPierre JouvelotSylvain RibsteinDorian Desblancs. The W-calculus: A Synchronous Framework for the Verified Modelling of Digital Signal Processing Algorithms
FARM 2021 - 9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design, Aug 2021, Virtual, South Korea. ⟨10.1145/3471872.3472970⟩
tel-02968939v1  Theses
Cédric Ho Thanh. Opetopes: Syntactic and Algebraic Aspects
Category Theory [math.CT]. Université de Paris, 2020. English
hal-03366644v1  Documents associated with scientific events
Cyril CohenThéo Zimmermann. A Nix toolbox for reproducible Coq environments, Continuous Integration and artifact reuse
The Coq Workshop, Jul 2021, Virtual, France
hal-02167423v1  Journal articles
Matthieu SozeauAbhishek AnandSimon BoulierCyril CohenYannick Forster et al.  The MetaCoq Project
Journal of Automated Reasoning, Springer Verlag, 2020, ⟨10.1007/s10817-019-09540-0⟩
hal-03371935v1  Conference papers
Abhishek DeLuc PellissierAlexis Saurin. Canonical proof-objects for coinductive programming: infinets with infinitely many cuts
PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming, Sep 2021, Tallinn, Estonia. pp.1-15, ⟨10.1145/3479394.3479402⟩
hal-02410910v1  Journal articles
Marina MilicevicDjordje BaralicJovana ObradovicZoran PetricMladen Zekic et al.  Proofs and surfaces
Annals of Pure and Applied Logic, Elsevier Masson, 2020, 171 (9), ⟨10.1016/j.apal.2020.102845⟩
hal-02408211v1  Directions of work or proceedings
David BaeldeAmy FeltyGopalan NadathurAlexis Saurin. A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller’s 60th birthday
Mathematical Structures in Computer Science, 29 (8), Cambridge University Press, pp.1007-1008, 2019, ⟨10.1017/S0960129519000136⟩
hal-03144849v4  Conference papers
Nuria BredeHugo Herbelin. On the logical structure of choice and bar induction principles
LICS 2021 - 36th Annual Symposium on Logic in Computer Science, Jun 2021, Rome / Virtual, Italy
hal-01962838v2  Conference papers
Cagdas BozmanBenjamin CanouRoberto Di CosmoPierrick CoudercLouis Gesbert et al.  Learn-OCaml : un assistant à l'enseignement d'OCaml
JFLA 2019 - Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France
hal-03103455v1  Conference papers
Kostia ChardonnetAlexis SaurinBenoît Valiron. Toward a Curry-Howard Equivalence for Linear, Reversible Computation
RC 2020 - 12th international conference on Reversible Computation, Jul 2020, Oslo / Virtual, Norway. pp.144-152, ⟨10.1007/978-3-030-52482-1_8⟩
hal-02557823v2  Conference papers
Hugo HerbelinÉtienne Miquey. A calculus of expandable stores
LICS 2020 - 35th ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken / Virtual, Germany. pp.564-577, ⟨10.1145/3373718.3394792⟩