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.

The grant amounts below are initial estimations and not necessarily the final amounts

7th call (12 November 2023)

  • Reconstructing AletheLF Proofs in Lambdapi application
    Visitor: Alessio Coltellacci
    Host: Yoni Zohar
    Grant: 3457 EUR
    Dates: 2024-04-01 to 2024-04-12

  • Learning for Automated Theorem Proving Based on Proof Structures in the Presence of a Large Proof Library application
    Visitor: Zsolt Zombori
    Host: Christoph Wernhard
    Grant: 1500 EUR
    Dates: 2024-04-01 to 2024-04-07

  • Interoperability of Tableaux and Sequent Calculus Proof Systems application
    Visitor: Simon Guilloud
    Host: Philipp Rümmer
    Grant: 2500 EUR
    Dates: 2024-03-25 to 2024-04-06

  • Towards 2-dimensional second-order algebraic theories application
    Visitor: Nathanael Arkor
    Host: Dylan McDermott
    Grant: 1916 EUR
    Dates: 2024-03-10 to 2024-03-16

  • Towards 2-dimensional 2nd-order algebraic theories application
    Visitor: Philip Saville
    Host: Dylan McDermott
    Grant: 1933 EUR
    Dates: 2024-03-10 to 2024-03-17

  • Checking proofs from QBF solvers in Dedukti and Lambdapi application
    Visitor: Martina Seidl
    Host: Catherine Dubois
    Grant: 1250 EUR
    Dates: 2024-02-19 to 2024-02-23

  • Expansion of the Goéland Theorem Prover and Interoperability with the LISA Proof Assistant application
    Visitor: Julie Cailler
    Host: Viktor Kuncak
    Grant: 3434 EUR
    Dates: 2024-02-19 to 2024-03-01

  • Conjecture and proof search in Agda with large language models application
    Visitor: Maximilian Doré
    Host: Moa Johansson
    Grant: 1220 EUR
    Dates: 2024-01-28 to 2024-02-02

  • Initial semantics for polymorphic type systems application
    Visitor: Benedikt Ahrens
    Host: Ambroise Lafont
    Grant: 1302 EUR
    Dates: 2024-01-21 to 2024-01-27

  • Translating from Lean to Dedukti application
    Visitor: Rishikesh Vaishnav
    Host: Sebastian Ullrich
    Grant: 1500 EUR
    Dates: 2024-01-15 to 2024-01-21

  • ω-categories, syntax and models application
    Visitor: Michele De Pascalis
    Host: Eric Finster
    Grant: 1606 EUR
    Dates: 2024-01-14 to 2024-01-20

6th call (8 May 2023)

  • Reconstruction of incomplete theorems and incomplete proofs with Larus application report
    Visitor: Salwa Tabet Gonzalez
    Host: Predrag Janicic
    Grant: 1587 EUR
    Dates: 2023-07-15 to 2023-07-22

  • Domain theory for program verification in Lean application report
    Visitor: Horatiu Cheval
    Host: Vlad Rusu
    Grant: 1159 EUR
    Dates: 2023-09-04 to 2023-09-10

  • Formal Specification and Verification of Attestation in Confidential Computing application report
    Visitor: Muhammad Usama Sardar
    Host: Lilia Georgieva
    Grant: 1583 EUR
    Dates: 2023-09-10 to 2023-09-14

  • Automatic verification of floating-point programs using Constrained Horn Solvers application report
    Visitor: Jasper Amilon
    Host: Philipp Rümmer
    Grant: 2284 EUR
    Dates: 2023-09-11 to 2023-09-22

  • Representation of Proofs via Hierarchical Higher-Order Port Graphs application report
    Visitor: Maribel Fernandez
    Host: Sandra Alves
    Grant: 1862 EUR
    Dates: 2023-09-12 to 2023-09-19

  • Using Coq to formalise differentiable logics for neural network application report
    Visitor: Natalia Slusarz
    Host: Alessandro Bruni
    Grant: 1478 EUR
    Dates: 2023-09-17 to 2023-09-23

  • Proof calculus for Real Algebraic Geometry application report
    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 report
    Visitor: Konstantinos Kogkalidis
    Host: Jean-Philippe Bernardy
    Grant: 1105 EUR
    Dates: 2023-09-05 to 2023-09-12

  • Translation of HOL4 proofs to Dedukti and Lambdapi application report
    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 report
    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 report
    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 report
    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 report
    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-15 to 2023-05-15

  • Computer science applications of Cubical Agda application report
    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 report
    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 report
    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 report
    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 report
    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 report
    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 report
    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 report
    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 report
    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