Software

  • Math-Components




    • The Mathematical Components library is a set of Coq libraries that cover the prerequisites for the mechanization of the proof of the Odd Order Theorem.





    • Alexey Solovyev (alexey.solovyev@inria.fr), Andrea Asperti (asperti@cs.unibo.it), Assia Mahboubi (assia.mahboubi@inria.fr), Cyril Cohen (cyril.cohen@inria.fr), Enrico Tassi (enrico.tassi@inria.fr), François Garillot (francois.garillot@inria.fr), Georges Gonthier (georges.gonthier@inria.fr), Ioana Pasca (ioana.pasca@inria.fr), Jeremy Avigad (jeremy.avigad@inria.fr), Laurence Rideau (laurence.rideau@inria.fr), Laurent Théry (laurent.thery@inria.fr), Russell O'Connor (r.oconnor@cs.ru.nl), Sidi Ould Biha (Sidi.Ould_Biha@inria.fr), Stéphane Le Roux (stephane.le.roux@ulb.ac.be), Yves Bertot (yves.bertot@inria.fr)



    • Assia Mahboubi (assia.mahboubi@inria.fr)



    • https://math-comp.github.io/
  • Coq



    • Coq is an interactive proof assistant based on the Calculus of (Co-)Inductive Constructions, extended with universe polymorphism. This type theory features inductive and co-inductive families, an impredicative sort and a hierarchy of predicative universes, making it a very expressive logic. The calculus allows to formalize both general mathematics and computer programs, ranging from theories of finite structures to abstract algebra and categories to programming language metatheory and compiler verification. Coq is organised as a (relatively small) kernel including efficient conversion tests on which are built a set of higher-level layers: a powerful proof engine and unification algorithm, various tactics/decision procedures, a transactional document model and, at the very top an integrated development environment (IDE).


    • Coq provides both a dependently-typed functional programming language and a logical formalism, which, altogether, support the formalisation of mathematical theories and the specification and certification of properties of programs. Coq also provides a large and extensible set of automatic or semi-automatic proof methods. Coq's programs are extractible to OCaml, Haskell, Scheme, …



    • Coq version 8.20 adds a new rewrite rule mechanism along with a few new features, a host of improvements to the virtual machine, the notation system, Ltac2 and the standard library.

    • An overview of the new features and changes, along with the full list of contributors is available at https://coq.inria.fr/refman/changes.html#version-8-20 .



    • Yves Bertot (Yves.Bertot@inria.fr), Frédéric Besson (frederic.besson@inria.fr), Tej Chajed (tchajed@mit.edu), Cyril Cohen (cyril.cohen@inria.fr), Pierre Corbineau (pierre.corbineau@imag.fr), Pierre Courtieu, Maxime Dénès (maxime.denes@inria.fr), Jim Fehrle (jim.fehrle@gmail.com), Julien Forest (julien.forest@ensiie.fr), Emilio Jesús Gallego Arias (e@x80.org), Gaëtan Gilbert (gaetan.gilbert@inria.fr), Georges Gonthier (Georges.Gonthier@inria.fr), Benjamin Grégoire (Benjamin.Gregoire@inria.fr), Jason Gross (jgross@mit.edu), Hugo Herbelin (Hugo.Herbelin@inria.fr), Vincent Laporte (vincent.laporte@inria.fr), Olivier Laurent (olivier.laurent@ens-lyon.fr), Assia Mahboubi (Assia.Mahboubi@inria.fr), Kenji Maillard (kenji.maillard@inria.fr), Érik Martin-Dorel (erik.martin-dorel@irit.fr), Guillaume Melquiond (guillaume.melquiond@inria.fr), Pierre-Marie Pedrot (Pierre-Marie.Pedrot@inria.fr), Clément Pit-Claudel, Kazuhiko Sakaguchi (kazuhiko.sakaguchi@inria.fr), Vincent Semeria (vincent.semeria@gmail.com), Michael Soegtrop (michael.soegtrop@intel.com), Arnaud Spiwack, Matthieu Sozeau (Matthieu.Sozeau@inria.fr), Enrico Tassi (Enrico.Tassi@inria.fr), Laurent Théry (laurent.thery@inria.fr), Anton Trunov (anton.a.trunov@gmail.com), Li-Yao Xia, Theo Zimmermann (theo.zimmermann@inria.fr)



    • Matthieu Sozeau (matthieu.sozeau@inria.fr)



    • http://coq.inria.fr/
  • Ssreflect



    • Ssreflect is tactic language that helps writing concise and uniform tactic based proof scripts for the Coq system. It was designed during the proofs of the 4 Color Theorem and the Feit-Thompson theorem.


    • Ssreflect is a tactic language extension to the Coq system, developed by the Mathematical Components team.





    • Assia Mahboubi (assia.mahboubi@inria.fr), Cyril Cohen (cyril.cohen@inria.fr), Enrico Tassi (Enrico.Tassi@inria.fr), Georges Gonthier (georges.gonthier@inria.fr), Laurence Rideau (Laurence.Rideau@inria.fr), Laurent Théry (Laurent.Thery@inria.fr), Yves Bertot (Yves.Bertot@inria.fr)



    • Yves Bertot (Yves.Bertot@inria.fr)



    • http://math-comp.github.io/math-comp/
  • Easycrypt




    • EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs. EasyCrypt can also be used for reasoning about differential privacy.



    • This software has not been the subject of new scientific developments, but has been maintained as it remains relevant in the team's context


      • Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, et al.. High-Assurance Cryptography in the Spectre Era. S&P 2021 – IEEE Symposium of Security and Privacy, May 2021, Virtual, France. ⟨10.1109/SP40001.2021.00046⟩. ⟨hal-03352062⟩
      • Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub. Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. CCS 2021 – ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2541-2563, ⟨10.1145/3460120.3484548⟩. ⟨hal-03469015⟩


    • Benjamin Grégoire (Benjamin.Gregoire@inria.fr), Gilles Barthe (Gilles.Barthe@inria.fr), Pierre-Yves Strub (pierre-yves.strub@inria.fr), Adrien Koutsos (adrien.koutsos@inria.fr)



    • Gilles Barthe (Gilles.Barthe@inria.fr)



    • https://github.com/EasyCrypt/easycrypt
  • Jasmin



    • Jasmin is a workbench for high-assurance and high-speed cryptography. Jasmin implementations aim at being efficient, safe, correct, and secure.

      Jasmin is both a language and a compiler from this language to assembly. The compiler is written and formally verified for correctness in the Coq proof assistant. This justifies that many properties can be proved on a source program and still apply to the corresponding assembly program: safety, termination, functional correctness…

      Jasmin comes with a set of tools to reason on Jasmin programs (a safety checker, a type-checker for Constant Time, a type-checker for Speculative Constant Time and an extraction to EasyCrypt to prove properties about the extracted Jasmin program, e.g. functional correctness).


    • The Jasmin programming language smoothly combines high-level and low-level constructs, so as to support “assembly in the head” programming. Programmers can control many low-level details that are performance-critical: instruction selection and scheduling, what registers to spill and when, etc. The language also features high-level abstractions (variables, functions, arrays, loops, etc.) to structure the source code and make it more amenable to formal verification. The Jasmin compiler produces predictable assembly and ensures that the use of high-level abstractions incurs no run-time penalty.

      The semantics is formally defined to allow rigorous reasoning about program behaviors. The compiler is formally verified for correctness (the proof is machine-checked by the Coq proof assistant). This ensures that many properties can be proved on a source program and still apply to the corresponding assembly program: safety, termination, functional correctness…

      Jasmin programs can be automatically checked for safety and termination (using a trusted static analyzer). The Jasmin workbench leverages the EasyCrypt toolset for formal verification. Jasmin programs can be extracted to corresponding EasyCrypt programs to prove functional correctness, cryptographic security, or security against side-channel attacks (constant-time).



    • On July 2024, a major release (2024.07.0) has been published.

    • This year, four minor versions and one major version have been released. Here
      are some of the most significant changes brought by these different versions.

      The semantics of the Jasmin language has been extended to cover more use cases.
      On one hand programmers no longer need to prove that memory accesses and
      (direct) array accesses are properly aligned. Jasmin programs have a
      well-defined semantics even if unaligned accesses occur. On the other hand more
      functions can have arrays as arguments and results.

      The programming language has been improved to simplify program writing tasks.
      Namespaces allow reusing names: two things may have the same name, as long as
      they belong to different namespaces. Spilling and unspilling of registers can
      now be done implicitly thanks to the spill and unspill operators. Type aliases
      can be defined through the new type key-word. Local variables may be initialized
      when declared.

      So as to give more security guaranties about the emitted code, the compiler can
      introduce code that zeroizes the stack at the end of export functions. The user
      can enable the feature with an annotation or a compiler flag.

      This is a minor release of Jasmin. Here is a brief description of a few of the
      changes it features.

      The checker for Constant-Time security, now available as a separate tool
      (jasmin-ct), has been made more precise and can also verify security in spite of
      speculative executions (Spectre).

      Support of x86 and ARMv7 architectures has been fostered. Many more instructions
      are available and some issues with large immediates have been fixed.


      • Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, et al.. Typing High-Speed Cryptography against Spectre v1. SP 2023- IEEE Symposium on Security and Privacy, IEEE, May 2023, San Francisco, United States. pp.1592-1609, ⟨10.1109/SP46215.2023.10179418⟩. ⟨hal-04106448⟩
      • José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, et al.. Formally verifying Kyber: Episode IV: Implementation correctness. CHES 2023 – Conference on Cryptographic Hardware and Embedded Systems, IACR, Sep 2023, Praha, Czech Republic. pp.164-193, ⟨10.46586/tches.v2023.i3.164-193⟩. ⟨hal-04218417⟩
      • José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, et al.. Formally verifying Kyber: Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. Crypto 2024, International Association for Cryptologic Research, Aug 2024, Santa Barbara (CA), United States. ⟨10.1007/978-3-031-68379-4_12⟩. ⟨hal-04595591v2⟩
      • Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, et al.. High-assurance zeroization. IACR Transactions on Cryptographic Hardware and Embedded Systems, 2024, 2024 (1), pp.375-397. ⟨10.46586/tches.v2024.i1.375-397⟩. ⟨hal-04691165⟩
      • Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya. Enforcing Fine-grained Constant-time Policies. CCS 2022 – 2022 ACM SIGSAC Conference on Computer and Communications Security, Nov 2022, Los Angeles CA, United States. pp.83-96, ⟨10.1145/3548606.3560689⟩. ⟨hal-03844366⟩
      • Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya. Structured Leakage and Applications to Cryptographic Constant-Time and Cost. CCS 2021 – ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.462-476, ⟨10.1145/3460120.3484761⟩. ⟨hal-03430789⟩
      • Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, et al.. High-Assurance Cryptography in the Spectre Era. S&P 2021 – IEEE Symposium of Security and Privacy, May 2021, Virtual, France. ⟨10.1109/SP40001.2021.00046⟩. ⟨hal-03352062⟩
      • José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, et al.. Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS 2019 – 26th ACM Conference on Computer and Communications Security, Nov 2019, London, United Kingdom. pp.1607-1622, ⟨10.1145/3319535.3363211⟩. ⟨hal-02404581⟩
      • José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, et al.. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. SP 2020 – 41st IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.965-982, ⟨10.1109/SP40000.2020.00028⟩. ⟨hal-02974993⟩
      • José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, et al.. Jasmin: High-Assurance and High-Speed Cryptography. CCS 2017 – Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, Oct 2017, Dallas, United States. pp.1-17. ⟨hal-01649140⟩


    • Alexandre Bourbeillon (alexandre.bourbeillon@loria.fr), Gaëtan Cassiers (gaetan.cassiers@uclouvain.be), Gilles Barthe (Gilles.Barthe@inria.fr), Benjamin Grégoire (Benjamin.Gregoire@inria.fr), Adrien Koutsos (adrien.koutsos@inria.fr), Vincent Laporte (vincent.laporte@inria.fr), Jean-Christophe Léchenet (jean-christophe.lechenet@inria.fr), Swarn Priya (swarn.priya@inria.fr), Santiago Arranz Olmos (santiago.arranz-olmos@mpi-sp.org)


    • The IMDEA Software Institute, Ecole Polytechnique, Universidade do Minho, Universidade do Porto, Max Planck Institute for Security and Privacy


    • Jean-Christophe Léchenet (jean-christophe.lechenet@inria.fr)



    • https://github.com/jasmin-lang/jasmin
  • MaskVerif




    • MaskVerif is a tool to verify the security of implementations protected against side channel attacks,
      in particular differential power analysis.
      It allows to check different security notions in the probing model:
      – Probing security
      – Non Interference
      – Strong Non Interference.
      The tool is able to analyse software implementations and hardware implementations (written in Verilog).
      It can prove the different security notions in presence of glitch or transition.







    • Benjamin Grégoire (benjamin.gregoire@inria.fr)



    • https://sites.google.com/view/maskverif/home
  • MaskComp




    • MaskComp is a compiler generating masked implementations protected against side channel attacks based on differential power analysis.
      It takes a unmasked program in a syntax close to C and generates a new C protected program.
      We do not claim that the generated C program will be secure after compilation (the C compiler may break protection), but
      it provides a good support for generating masked implementation.







    • Benjamin Grégoire (benjamin.gregoire@inria.fr)



    • https://sites.google.com/site/maskingcompiler/home
  • AutoGnP




    • autoGnP is an automated tool for analyzing the security of padding-based public-key encryption schemes (i.e. schemes built from trapdoor permutations and hash functions). This years we extended the tool to be able to deal with schemes based on cyclic groups and bilinear maps.





    • Benjamin Grégoire (Benjamin.Gregoire@inria.fr), Gilles Barthe (Gilles.Barthe@inria.fr), Pierre-Yves Strub (pierre-yves.strub@inria.fr)



    • Gilles Barthe (Gilles.Barthe@inria.fr)



    • https://github.com/ZooCrypt/AutoGnP
  • coq-elpi



    • Coq-elpi provides a Coq plugin that embeds ELPI. It also provides a way to embed Coq terms into lambdaProlog using the Higher-Order Abstract Syntax approach (HOAS) and a way to read terms back. In addition to that it exports to ELPI a set of Coq primitives, e.g. printing a message, accessing the environment of theorems and data types, defining a new constant and so on. For convenience it also provides a quotation and anti-quotation for Coq's syntax in lambdaProlog. E.g. {{nat}} is expanded to the type name of natural numbers, or {{A -> B}} to the representation of a product by unfolding the -> notation. Finally it provides a way to define new vernacular commands and new tactics.


    • Coq plugin embedding ELPI



    • Coq-Elpi commands to assemble programs and tactics were revised
      so to better support the separation of parsing from execution
      introduced in Coq 8.18 and also to take advantage of the new
      incremental compilation offered by Elpi.

    • – parsing/execution separation


      • Enrico Tassi. Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq. ITP 2019 – 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨10.4230/LIPIcs.CVIT.2016.23⟩. ⟨hal-01897468v2⟩
      • Enrico Tassi. Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect). The Fourth International Workshop on Coq for Programming Languages, Jan 2018, Los Angeles (CA), United States. ⟨hal-01637063⟩
      • Davide Fissore, Enrico Tassi. Higher-Order unification for free!. PPDP 2024: 26th International Symposium on Principles and Practice of Declarative Programming, Sep 2024, Milan, Italy. pp.1-13, ⟨10.1145/3678232.3678233⟩. ⟨hal-04547069v4⟩
      • Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi. Practical and sound equality tests, automatically — Deriving eqType instances for Jasmin’s data types with Coq-Elpi. CPP ’23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2023, Boston MA USA, France. pp.167-181, ⟨10.1145/3573105.3575683⟩. ⟨hal-03800154⟩


    • Enrico Tassi (Enrico.Tassi@inria.fr), Davide Fissore (davide.fissore@inria.fr)



    • Enrico Tassi (enrico.tassi@inria.fr)




    •
  • ELPI



    • Elpi implements a variant of lambdaProlog enriched with Constraint Handling Rules.

      Being a descendant of Prolog, Elpi is a rule-based language, meaning that its programs are structured as sets of rules that dictate how computations proceed.
      These rules can be introduced in two ways: dynamically and statically.
      Dynamic rules are introduced at runtime, particularly when processing binders, to attach data to bound variables in a scoped and context-sensitive manner.
      Static rules are extended or updated as the logical environment or Rocq evolves, ensuring compatibility with new definitions and proofs as they are added.

      Constraints and their handling rules are used to enrich unification variables (holes) with meta data, for example their type. Handling rules are instrumental to maintain the consistency of the constraint store, for example detecting incompatible type assignments for the same hole.


    • Elpi is a high-level programming language designed to implement new commands and tactics for the Rocq prover. It provides native support for syntax trees with binders and holes, relieving programmers of the complexities associated with De Bruijn indices and unification variables.



    • Elpi's backend was completely rewritten in order to obtain faster
      compilation and perform type checking early in the compilation
      pipeline, paving the way to more static analysis. In particular
      D. Fissore is working on mode and determinacy analysis on top
      of the new type checking phase.

    • – Faster separate compilation/linking


      • Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi. Practical and sound equality tests, automatically — Deriving eqType instances for Jasmin’s data types with Coq-Elpi. CPP ’23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2023, Boston MA USA, France. pp.167-181, ⟨10.1145/3573105.3575683⟩. ⟨hal-03800154⟩
      • Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi. ELPI: fast, Embeddable, λProlog Interpreter. Proceedings of LPAR, Nov 2015, Suva, Fiji. ⟨hal-01176856⟩
      • Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi. Implementing Type Theory in Higher Order Constraint Logic Programming. Mathematical Structures in Computer Science, 2019, 29 (8), pp.1125-1150. ⟨hal-01410567v3⟩
      • Enrico Tassi. Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq. ITP 2019 – 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨10.4230/LIPIcs.CVIT.2016.23⟩. ⟨hal-01897468v2⟩


    • Enrico Tassi (Enrico.Tassi@inria.fr), Claudio Sacerdoti Coen (claudio.sacerdoticoen@unibo.it)



    • Enrico Tassi (enrico.tassi@inria.fr)



    • https://github.com/lpcic/elpi/
  • Semantics




    • A didactical Coq development to introduce various semantics styles. Shows how to derive an interpreter, a compiler, a verifier, or a program analyser from formal descriptions, and how to prove their consistency.

      This is a library for the Coq system, where the description of a toy programming language is presented. The value of this library is that it can be re-used in classrooms to teach programming language semantics or the Coq system. The topics covered include introductory notions to domain theory, pre and post-conditions, abstract interpretation, compilation, and the proofs of consistency between all these points of view on the same programming language. Standalone tools for the object programming language can be derived from this development.



    • This version now contains an example of small compiler and a partial correctness proof (completeness).



    • Christine Paulin (Christine.Paulin@lri.fr), Yves Bertot (Yves.Bertot@inria.fr)



    • Yves Bertot (Yves.Bertot@sophia.inria.fr)



    • https://github.com/coq-community/semantics
  • CoqInterval




    • CoqInterval is a library for the proof assistant Coq.

      It provides several tactics for proving theorems on enclosures of real-valued expressions. The proofs are performed by an interval kernel which relies on a computable formalization of floating-point arithmetic in Coq.

      The Marelle team developed a formalization of rigorous polynomial approximation using Taylor models in Coq. In 2014, this library has been included in CoqInterval.




      • Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux. Enabling Floating-Point Arithmetic in the Coq Proof Assistant. Journal of Automated Reasoning, 2023, 67 (33), ⟨10.1007/s10817-023-09679-x⟩. ⟨hal-04114233v2⟩
      • Florian Faissole, Paul Geneau de Lamarlière, Guillaume Melquiond. End-to-End Formal Verification of a Fast and Accurate Floating-Point Approximation. 15th International Conference on Interactive Theorem Proving, Sep 2024, Tbilisi, Georgia. pp.14:1-14:18, ⟨10.4230/LIPIcs.ITP.2024.14⟩. ⟨hal-04515714v3⟩
      • Guillaume Melquiond. Turning the Coq Proof Assistant into a Pocket Calculator. Coq 2024 – 15th Coq Workshop, Sep 2024, Tbilisi, Georgia. ⟨hal-04702129⟩
      • Guillaume Melquiond. Plotting in a Formally Verified Way. Proceedings of the 6th Workshop on Formal Integrated Development Environment, May 2021, Online, United States. pp.39-45, ⟨10.4204/EPTCS.338.6⟩. ⟨hal-03168208v2⟩
      • Guillaume Melquiond. Formal Verification for Numerical Computations, and the Other Way Around. Computer Arithmetic. Université Paris Sud, 2019. ⟨tel-02194683⟩
      • Paul Geneau de Lamarlière. Vérification de bout en bout d’une fonction de bibliothèque mathématique. JFLA 2025 – 36es Journées Francophones des Langages Applicatifs, Jan 2025, Roiffé, France. ⟨hal-04859533⟩
      • Guillaume Melquiond. Proving bounds on real-valued functions with computations. International Joint Conference on Automated Reasoning, IJCAR 2008, Aug 2008, Sydney, Australia. pp.2–17, ⟨10.1007/978-3-540-71070-7_2⟩. ⟨hal-00180138⟩
      • Guillaume Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, 2012, 216, pp.14-23. ⟨10.1016/j.ic.2011.09.005⟩. ⟨hal-00797913⟩
      • Érik Martin-Dorel, Guillaume Melquiond. Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. Journal of Automated Reasoning, 2016, 57 (3), pp.187-217. ⟨10.1007/s10817-015-9350-4⟩. ⟨hal-01086460v2⟩
      • Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. Interactive Theorem Proving, Aug 2016, Nancy, France. ⟨10.1007/978-3-319-43144-4_17⟩. ⟨hal-01289616v2⟩
      • Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. Journal of Automated Reasoning, 2019, 62 (2), pp.281-300. ⟨10.1007/s10817-018-9463-7⟩. ⟨hal-01630143v2⟩


    • Pierre Roux (pierre.roux@onera.fr), Paul Geneau De Lamarliere (paul.geneau-de-lamarliere@inria.fr), Assia Mahboubi (assia.mahboubi@inria.fr), Érik Martin-Dorel (erik.martin-dorel@irit.fr), Guillaume Melquiond (guillaume.melquiond@inria.fr), Jean-Michel Muller (jean-michel.muller@inria.fr), Laurence Rideau (laurence.rideau@inria.fr), Laurent Théry (laurent.thery@inria.fr), Micaela Mayero (mayero@lipn.univ-paris13.fr), Mioara Joldes (joldes@laas.fr), Nicolas Brisebarre (nicolas.brisebarre@inria.fr), Thomas Sibut-Pinote (thomas.sibut-pinote@inria.fr)



    • Guillaume Melquiond (guillaume.melquiond@inria.fr)



    • https://coqinterval.gitlabpages.inria.fr/
  • VsCoq




    • VsCoq is an extension for Visual Studio Code (VS Code) and VSCodium which provides support for the Coq Proof Assistant.

      VsCoq is distributed in two flavours:

      – VsCoq Legacy (required for Coq < 8.18, compatible with Coq >= 8.7) is based on the original VsCoq implementation by C.J. Bell. It uses the legacy XML protocol spoken by CoqIDE.

      – VsCoq (recommended for Coq >= 8.18) is a full reimplementation around a language server which natively speaks the LSP protocol.



    • We have mainly been working on stability and bug fixes, reaching parity with the legacy branch VSCoq 1.
      Moreover the Goal view features an efficient rendering algorithm that runs client side and the overall performance of the language server was greatly improved on large files. We also wrote onboarding documentation.

    • We have mainly been working on stability and bug fixes, in this release you’ll find :

      – Some improvements to performance on large files.
      – Fixing document state invalidation bugs.
      – Goal view improvements.





    • Romain Tetley (romain.tetley@inria.fr)



    • https://github.com/coq/vscoq