The HoTT library is a formalization of homotopy type theory using proof assistant Coq. In it, there are many theorems from the HoTT book and it also has some results using higher inductive types. Link to formalization
The main publication:
Publications by EUTYPES members related to parts of the library:
Publications by EUTYPES members building on top of the library (sources elsewhere):
Unimath is a formalization of mathematics in univalent foundations using the proof assistant Coq. Among others, it contains numerous results on (bi)category theory, K-theory, substitution systems, and induction schemes. Link to formalization
Some contributions by EUTYPES members:
Cubical Agda is a formalization of cubical type theory using the proof assistant Agda. it supports higher inductive types and definitional computation rules of the univalence axiom. Link to formalization
Maintainers: Anders Mörtberg (CMU and Stockholm University) and Andrea Vezzosi (IT University Copehagen)
Formalisation of two models of Bitcoin in Agda by Anton Setzer. It formalises the blockchain structure of Bitcoin by formalising it as a ledger like a bank account and as a transaction dag. The models are designed to be used for verification of the correctness of the blockchain and verifying smart contracts.
Link to the formalization and Link to the publication.
Feature Agda is a framework for specifying and proving properties of feature-based composition of workflows implemented in the Feature-Oriented Software Production Lines paradigm. It is developed by Stephan Adelsberger, Anton Setzer, and Erik Walkingshaw.
Link to formalization and Link to the publication.
Development of a library for writing graphical user interfaces using object-based programming techniques in the theorem prover Agda. It is developed by Stephan Adelsberger, Anton Setzer, and Erik Walkingshaw. An application for the prescription of anticoagulants in the healthcare domain was created in collaboration with the Medical University of Vienna. Prescription of anticoagulants has been shown to be highly error-prone when followed manually. This library develops an application to support the prescription and proves medically relevant safety properties of the resulting GUI.
There are two repositories for this library, which can be found here and [[https://github.com/stephanpaper/SETTA18|here]. More information can be found in the following papers:
OOagda is a library for writing object-based programs in Agda by Andreas Abel, Stephan Adelsberger, and Anton Setzer. The library allows to write graphical user interfaces in the theorem prover Agda. State dependent interactive programs and objects are formulated as well which avoid the use of exception handling. In the paper, examples of GUI are presented.
Link to formalization and link to publication.
This is a library for formalising processes of the process algebra CSP in Agda and it is developed by Bashar Igried and Anton Setzer. It formalises CSP processes in Agda and implements trace semantics trace and stable failure semantics of CSP in Agda. Several laws of CSP are shown in Agda using this library.
Link to formalization and relevant papers:
ReLoC is a mechanized logic for interactively proving contextual refinements of programs in a language with higher-order state, fine-grained concurrency, polymorphism and existential and recursive types. It is build on top of the Iris framework in Coq.
This formalization provides a semantics of a subset of C that takes the C standard's unspecified evaluation order and undefined behavior due to sequence point violations into account. The formalization is build on top of the Iris framework in Coq and comes with a separation logic and verification condition generator (vcgen).
Iron is a higher-order concurrent separation logic that allows for precise reasoning about resources that are transferable among dynamically allocated threads. The formalization is build on top of the Iris framework in Coq.
Std++ is an extended "standard library" for Coq that provides extensive support for common data structures such as lists, finite maps, finite sets, and finite multisets. It is entirely dependency- and axiom-free, and uses type classes for overloading of notations and abstraction.
A translation from Extensional Type Theory to Intensional Type Theory in a constructive way. It comes with a proof-of-concept « plugin » to write extensional proofs in Coq to inhabit Coq types. Link to formalization
Authors: Matthieu Sozeau, Nicolas Tabarau, and Theo Winterhalter (INRIA)
Meta-programming in Coq. It contains in particular a specification of the proof-assistant with work-in-progress proofs of parts of the system and certification of its implementation. It also features a plugin to quote and reify actual Coq terms to and from the reflected syntax. Link to formalization
A formalisation of the Java Virtual Machine that contains the semantics description for all mnemonics of the Java bytecode. Link to web page
by Wilmer Ricciotti (University of Edinburgh) and James Cheney (University of Edinburgh and The Alan Turing Institute)
A mechanization of the semantics of SQL with set/bag operations, nested subqueries, and nulls, written in Coq. This formalization can be used to reason about the correctness of rewrite rules (widely applied in commercial databases to convert a user query into an equivalent one that can be executed more efficiently).
Setoid type theory is a joint project with participants from Nottingham (UK), Nantes (France) and Budapest (Hungary) aiming to develop a new proof assistant for extensional type theory. We have a prototype proof assistant for setoid type theory. Link to prototype proof assistant
A new method for formalising metatheoretical results about type theory reusing existing implementations of type theory.
Publication: Ambrus Kaposi, András Kovács, Nicolai Kraus: Shallow Embedding of Type Theory is Morally Correct. MPC 2019: 329-365.
Using this, we have the currently known most complete formalisation of canonicity for Martin Löf's type theory. Link to formalization
Mathematical Components is an extensive and coherent repository of formalized mathematical theories. It is based on the Coq proof assistant, powered with the Coq/SSReflect language. It is the cornerstone of an ecosystem of experimental extensions. Contributions in the period, by members of the team or by others include a library formalized classical analysis, support for ordered structures and support for finite sets.
This is an experimental library for real analysis for the Coq proof-assistant and using the Mathematical Components library. This is collective work by Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi, and Pierre-Yves Strub. This formal development is available here.
High level commands to declare and evolve a hierarchy based on packed classes, as advocated in the mathematical components library for Coq. This is work by Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. This formal development is available here.
This library describes a transformation on polynomials that makes it easier to compute polynomials whose roots are the sum or products of roots of other polynomials. The authors are Boris Djalal and Cyril Cohen. This formal development is available here.
This library describes an algorithm to compute the value of an hexa-decimal digit of pi without computing the digits that precede it. It is based on the mathematical components and coquelicot libraries for Coq. The authors are Laurence Rideau and Laurent Théry. This formal development is available .
This library describes an algorithm to compute the value pi using an algorithm that was made populare in the 1970s and is now used in mpfr, for example. The development is based on the coquelicot library for Coq. The author is Yves Bertot. This formal development is available here.
This library describes an algorithm to compute triangulations of a set of points in the plane. The author is Yves Bertot. This formal development is available here.
This library describes the formal verification of a C function that computes the square root of IEEE floating point numbers. The verification is comprehensive in that it provides guarantees about a C implementation, showing that under some conditions no abnormal result are produced (infinities of NaNs) and that the result is reasonably close to the expected mathematical value (within a distance 5 / 2 ^ 23 times the expected value). The authors are Andrew Appel and Yves Bertot. This formal development is available here, branch "abstract-float-size".
This library provides a formal correctness proofs for comparison algorithms in Binary 64 and Decimal 64 floating point formats. The authors are Arthur Blot, Jean-Michel Muller, and Laurent Théry. This formal development is available here.
Jasmin is a compiler specialized for the implementation of cryptographic primitives, with a particular attention to avoid hidden channels. The authors are Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Benedikt Schmidt, and Pierre-Yves Strub. This formal development is available here.
FCSL is the first completely formalized framework for mechanized verification of full functional correctness of fine-grained concurrent programs. It is implemented as an embedded domain-specific language (DSL) in the dependently-typed language of the Coq proof assistant, and is powerful enough to reason about programming features such as higher-order functions and local thread spawning. By incorporating a uniform concurrency model, based on state-transition systems and partial commutative monoids (PCM), FCSL makes it possible to build proofs about concurrent libraries in a thread-local, compositional way, thus facilitating scalability and reuse: libraries are verified just once, and their specifications are used ubiquitously in client-side reasoning.
This project site provides access to the Coq-based development of FCSL as a logic and as a verification framework. The development includes the description of the logic's semantic domain, denotations of effectful statements and types, as well as structural lemmas, playing the role of the logic's inference rules.
The PCM subpart of the framework has been released on OPAM package manager. The source code is available on GitHub at fcsl-pcm.
https://software.imdea.org/fcsl/ and https://doi.org/10.5281/zenodo.3365991
