European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

6th call (8 May 2023)

  • Proof calculus for Real Algebraic Geometry application
    Visitor: Lucas Michel
    Hosts: James Davenport and Matthew England
    Grant: 2702 EUR
    Dates: 2023-08-28 to 2023-09-08

  • Neural Premise Selection for Agda application
    Visitor: Konstantinos Kogkalidis
    Host: Jean-Philippe Bernardy
    Grant: 1105 EUR
    Dates: 2023-09-11 to 2023-09-15

  • Translation of HOL4 proofs to Dedukti and Lambdapi application
    Visitor: Frédéric Blanqui
    Host: Magnus Myreen
    Grant: 1421 EUR
    Dates: 2023-05-22 to 2023-05-26

  • Machine-learned premise selection for Agda: the prover’s infrastructure application
    Visitor: Orestis Melkonian
    Host: Jean-Philippe Bernardy
    Grant: 1092 EUR
    Dates: 2023-06-19 to 2023-06-21

  • SMT solving and proofs for non-linear arithmetic application
    Visitor: Jasper Nalbach
    Host: James Davenport and Matthew England
    Grant: 2702 EUR
    Dates: 2023-08-28 to 2023-09-08

  • An interface for category theory in coq, applied to univalent foundations application
    Visitor: Luc Chabassier
    Host: Benedikt Ahrens
    Grant: 2082 EUR
    Dates: 2023-09-04 to 2023-09-15

5th call (1 March 2023)

  • Categorical semantics for propositional dependent type theories application
    Visitor: Matteo Spadetto (University of Leeds, UK)
    Host: Benno van den Berg (Institute for Logic, Language and Computation - ILLC, Amsterdam, Netherlands)
    Grant: 2604 EUR
    Dates: 2023-04-09 to 2023-04-30

  • Computer science applications of Cubical Agda application
    Visitor: Axel Ljungström (Stockholm University, Sweden)
    Host: Stefano Berardi (University of Turin, Italy)
    Grant: 2369 EUR
    Dates: 2023-04-26 to 2023-05-05

  • Formal Specification and Verification of Attestation in Confidential Computing application
    Visitor: Muhammad Usama Sardar (Chair of Systems Engineering, Dresden, Germany)
    Host: Lilia Georgieva (Heriot-Watt University, Edinburgh, UK)
    Grant: 2041 EUR
    Dates: 2023-05-14 to 2023-05-20

  • Coinductive proof search for inhabitation of quantitative types application
    Visitor: Jose Espirito Santo (University of Minho, Braga, Portugal)
    Host: Delia Kesner (IRIF, Paris, France)
    Grant: 1355 EUR
    Dates: 2023-05-21 to 2023-05-27

  • Liquid Monadic Intersection Types application
    Visitor: Riccardo Treglia (Università di Bologna, Italy)
    Host: Mário Florido (University of Porto, Portugal)
    Grant: 1990 EUR
    Dates: 2023-05-21 to 2023-05-31

  • Understanding interpretations of HoTT in elementary (oo,1)-toposes application
    Visitor: Morgan Elliot Rogers (CNRS, Villetaneuse, France)
    Host: Paige Randall North (Utrecht University, Netherlands)
    Grant: 2459 EUR
    Dates: 2023-05-22 to 2023-06-04

4th call (1 January 2023)

  • Translation from Dedukti to Minlog application report
    Visitor: Yoan Géran (MINES ParisTech, Fontainebleau, France)
    Host: Helmut Schwichtenberg (Mathematisches Institut der Universität München, Germany)
    Grant: 1478 EUR
    Dates: 2023-02-05 to 2023-02-12

  • Static Guarantees of Confluence in Actor Languages application
    Visitor: Violet Ka I Pun (Western Norway University of Applied Sciences, Bergen, Norway)
    Host: Ludovic Henrio (LIP Laboratory, ENS Lyon)
    Grant: 1500 EUR
    Dates: 2023-04-16 to 2023-04-23

  • Comparing notions of dependent algebraic theory application report
    Visitor: Peter Lumsdaine (Stockholm University, Sweden)
    Host: Benedikt Ahrens (Delft University of Technology, Netherlands)
    Grant: 1363 EUR
    Dates: 2023-03-18 to 2023-03-25

  • Proof automation in Cubical Agda application report
    Visitor: Maximilian Doré (University of Oxford, UK)
    Host: Anders Mörtberg (Stockholm University, Sweden)
    Grant: 1192 EUR
    Dates: 2023-02-27 to 2023-03-03

  • Automated Translation of Mizar Declarative Proof application
    Visitor: Karol Pak (Institute of Computer Science, Bialystok, Poland)
    Host: Cezary Kaliszyk (University of Innsbruck, Austria)
    Grant: 2922 EUR
    Dates: 2023-04-17 to 2023-05-06

  • Larus/Dedukti application
    Visitor: Julien Narboux (University of Strasbourg, France)
    Host: Predrag Janicic (University of Belgrade, Serbia)
    Grant: 1020 EUR
    Dates: 2023-05-02 to 2023-05-05

  • Termination Checking of Real-World Programs Using Term Rewriting Systems application report
    Visitor: Dragana Milovancevic (EPFL, Switzerland)
    Host: Carsten Fuhs (Birkbeck, University of London, UK)
    Grant: 1450 EUR
    Dates: 2023-03-10 to 2023-03-27

  • Translation of Generic Symbolic Execution Steps into Dedukti application report
    Visitor: Dorel Lucanu (Alexandru Ioan Cuza University, Romania)
    Host: Gilles Dowek (Ecole Normale Superieure Paris-Saclay, France)
    Grant: 1835 EUR
    Dates: 2023-03-20 to 2023-04-01

  • Indexing and retrieval of formal proofs in an heterogeneous settings application
    Visitor: Claudio Sacerdoti Coen (Alma Mater Studiorum - Università di Bologna, Italy)
    Host: Frédéric Blanqui (Ecole Normale Superieure Paris-Saclay, France)
    Grant: 1037 EUR
    Dates: 2023-04-16 to 2023-04-21

3rd call (1 July 2022)

  • Behavioural Types for Smart Contracts application report
    Visitor: Emilio Tuosto (Gran Sasso Science Institute, L’Aquila, IT)
    Host: Antonio Ravara (Universidade NOVA de Lisboa, Lisbon, PT)
    Grant: 1500 EUR
    Dates: 2022-07-14 to 2022-07-22

  • Leveraging a λProlog engine for type class resolution in Coq and Lambdapi application report
    Visitor: Matteo Manighetti (INRIA Saclay, Palaiseau, FR)
    Host: Enrico Tassi (Inria Université Côte d’Azur, Valbonne , FR)
    Grant: 1700 EUR
    Dates: 2022-10-15 to 2022-10-29

  • Evaluation efficiency in cubical type theories application report
    Visitor: András Kovács (Eötvös Loránd University, Budapest, HU)
    Host: Anders Mörtberg (Stockholm University, SE)
    Grant: 1040 EUR
    Dates: 2022-10-09 to 2022-10-16

  • Hierarchical Higher-Order Port Graphs for the representation and analysis of proofs application report
    Visitor: Maribel Fernandez (King’s College London, GB)
    Host: Sandra Alves (University of Porto, PT)
    Grant: 902 EUR
    Dates: 2022-09-12 to 2022-09-18

  • Unification Library & Mechanized Type Inference in Agda application report
    Visitor: Luca Ciccone (Università di Torino, IT)
    Host: Ornela Dardha (University of Glasgow, GB)
    Grant: 2450 EUR
    Dates: 2022-09-04 to 2022-09-18

2nd call (3 April 2022)

  • Using “behavioural types” for automatic validation of distributed systems application report
    Visitor: Paola Giannini (Università del Piemonte Orientale, Alessandria, IT)
    Host: Laura M. Castro (Universidade da Coruña, ES)
    Grant: 1800 EUR
    Dates: 2022-09-19 to 2022-09-30

  • Formalisation of Meaning Explanations in Agda application report
    Visitor: Anton Setzer (Swansea University, GB)
    Host: Peter Dybjer (Chalmers University of Technology, Gothenburg, SE)
    Grant: 1520 EUR
    Dates: 2022-08-23 to 2022-09-06

  • Towards Reliable Distributed Graph Databases: Automated Verification of a Conflict-Free Replicated Property Graph Data Structure application report
    Visitor: Stefania Dumbrava (ENSIIE, Evry, FR)
    Host: Mario Pereira (NOVA Universidade Lisboa, PT)
    Grant: 1300 EUR
    Dates: 2022-07-12 to 2022-07-21

  • Rechecking KProver proof objects into Dedukti application report
    Visitor: Amelie Ledein (Inria Saclay, Palaiseau, FR)
    Hosts: Traian Serbanuta and Dorel Lucanu (University of Bucharest, RO)
    Grant: 1520 EUR
    Dates: 2022-07-04 to 2022-07-17

  • Quantitative Types for Programming Languages with Global State application report
    Visitor: Delia Kesner (Universite de Paris, FR)
    Host: Sandra Alves (Universidade do Porto, PT)
    Grant: 960 EUR
    Dates: 2022-07-03 to 2022-07-08

  • Mechanized Type Inference in the Linear π-Calculus application report
    Visitor: Luca Ciccone (Università di Torino, IT)
    Host: Ornela Dardha (University of Glasgow, GB)
    Grant: 1200 EUR
    Dates: 2022-05-22 to 2022-05-29

1st call (18 January 2022)

  • Infrastructure for Automated Theorem Provers Inventory application report
    Visitor: Alexander Steen (University of Greifswald, DE)
    Host: Pascal Fontaine (University of Liège, BE)
    Grant: 1550 EUR
    Dates: 2022-07-07 to 2022-07-13

  • Sabanci Coq Workshop and Research Visit application report
    Visitor: Emilio Jesús Gallego Arias (Inria, Paris, FR)
    Host: Suha Orhun Mutluergil (Sabanci University, Istanbul, TR)
    Grant: 1400 EUR
    Dates: 2022-09-01 to 2022-09-10

  • Algebraic Session Types application report
    Visitor: Andreia Mordido (Faculdade de Ciências, Universidade de Lisboa, PT)
    Host: Peter Thiemann (Technical Faculty, Freiburg University, DE)
    Grant: 1200 EUR
    Dates: 2022-05-30 to 2022-06-06

  • Compiling dependent pattern matching to elimination principles in Dedukti application report
    Visitor: Thiago Felicissimo (Faculté des Sciences d’Orsay, FR)
    Host: Jesper Cockx (TU Delft, NL)
    Grant: 1500 EUR
    Dates: 2022-05-08 to 2022-05-21

  • A bootstrapping verified compiler for a concurrent functional language: the design application report
    Visitor: Gergely Buday (Institute of Technology, Gyöngyös, HU)
    Host: Alcides Fonseca (LASIGE, Faculdade de Ciências da Universidade de Lisboa, PT)
    Grant: 1000 EUR
    Dates: 2022-04-11 to 2022-04-15

  • Signatures for second-order essentially algebraic theories
    Visitor: Rafaël Bocquet (Eötvös Loránd University, Budapest, HU)
    Host: Christian Sattler (Chalmers University of Technology, Gothenburg, SE)
    Grant: 1600 EUR
    Dates: 2022-03-30 to 2022-04-09