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.

11th call (31st July 2024)

  • Comodule representations of second-order functionals application
    Visitor: Danel Ahman
    Host: Andrej Bauer
    Grant: 2850 EUR
    Dates: 2024-09-09 to 2024-09-24

  • Strictification of the syntax of type theory application
    Visitor: Loïc Pujet
    Host: Ambrus Kaposi
    Grant: 1430 EUR
    Dates: 2024-09-02 to 2024-09-06

  • Concurrency in cubical type theory application report
    Visitor: Thorsten Altenkirch
    Host: Tarmo Uustalu
    Grant: 2033 EUR
    Dates: 2024-08-31 to 2024-09-06

  • Modern algebraic perspectives on the λ-calculus and its extensions application report
    Visitor: Nathanael Arkor
    Host: Martin Hyland
    Grant: 1750 EUR
    Dates: 2024-08-11 to 2024-08-18

  • Modern algebraic perspectives on the λ-calculus and its extensions application report
    Visitor: Dylan McDermott
    Host: Martin Hyland
    Grant: 1710 EUR
    Dates: 2024-08-11 to 2024-08-18

  • Exploring anti-unification over typed languages and equational theories application report
    Visitor: David Cerna
    Host: Temur Kutsia
    Grant: 1800 EUR
    Dates: 2024-08-01 to 2024-08-10

10th call (1st May 2024)

  • Challenges in the Formal Verification of Attested TLS in Confidential Computing application report
    Visitor: Muhammad Usama Sardar
    Host: Lilia Georgieva
    Grant: 2264 EUR
    Dates: 2024-08-25 to 2024-08-31

  • A type theory for exact and continuous Bayesian observations application report
    Visitor: Mario Román
    Host: Elena Di Lavore
    Grant: 1349 EUR
    Dates: 2024-06-10 to 2024-06-14

  • A new axiomatization for synthetic differential geometry application report
    Visitor: Felix Cherubini
    Host: Ulrik Buchholtz
    Grant: 1924 EUR
    Dates: 2024-06-23 to 2024-06-29

  • A rethinking of a Prolog interpreter based on a three-valued logic using Maude application report
    Visitor: João Barbosa
    Host: Santiago Escobar
    Grant: 1057 EUR
    Dates: 2024-07-21 to 2024-07-27

  • Coupling SMT and theorem proving to prove hardware/software security mechanisms application report
    Visitor: Volker Stolz
    Host: Guillaume HIET
    Grant: 1939 EUR
    Dates: 2024-09-01 to 2024-09-11

9th call (17th March 2024)

  • Auditable Constraint Programming: Integrating Proof Logging with Fuzzing and Explanations application report
    Visitor: Matthew McIlree
    Host: Tias Guns
    Grant: 2200 EUR
    Dates: 2024-07-07 to 2024-07-15

  • Second-Order Generalised Algebraic Theories for Modal and Substructural Type Theories application report
    Visitor: Jacob Neumann
    Host: Ambrus Kaposi
    Grant: 1777 EUR
    Dates: 2024-06-24 to 2024-07-02

  • Coinduction in Cubical Agda application report
    Visitor: Stefania Damato
    Host: Anders Mortberg
    Grant: 2181 EUR
    Dates: 2024-06-19 to 2024-06-27

  • Higher-order effectful programming languages and quantitative type system application report
    Visitor: Sandra Alves
    Host: Delia Kesner
    Grant: 1516 EUR
    Dates: 2024-06-16 to 2024-06-22

  • Evaluation and development of the Alk platform for enhancing students’ algorithm design and analysis skills application report
    Visitor: Oana Andrei
    Host: Dorel Lucanu
    Grant: 2131 EUR
    Dates: 2024-05-13 to 2024-05-21

8th call (7th January 2024)

  • Domain theory for program verification in Lean application report
    Visitor: Horatiu Cheval
    Host: Vlad Rusu
    Grant: 1230 EUR
    Dates: 2024-06-10 to 2024-06-15

  • Proof Theory for Programmers: Promoting Output of Theorem Provers to Formative Feedback for Computer Science Students application report
    Visitor: Ján Perháč
    Host: Michael Kirkedal Thomsen
    Grant: 1650 EUR
    Dates: 2024-06-01 to 2024-06-09

  • Computer-Assisted Proof Verification for Higher-Order Automated Reasoning within the Dedukti Framework application report
    Visitor: Melanie Taprogge
    Host: Frédéric Blanqui
    Grant: 2433 EUR
    Dates: 2024-03-25 to 2024-04-07

  • Bidimensional Markov categories application report
    Visitor: Elena Di Lavore
    Host: Mario Roman Garcia
    Grant: 1694 EUR
    Dates: 2024-03-10 to 2024-03-16

  • Propositional containers and reductions in computability theory application report
    Visitor: Danel Ahman
    Host: Andrej Bauer
    Grant: 2808 EUR
    Dates: 2024-02-25 to 2024-03-09

7th call (12th November 2023)

  • Learning for Automated Theorem Proving Based on Proof Structures in the Presence of a Large Proof Library application report
    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 report
    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 report
    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 report
    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 report
    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 report
    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 report
    Visitor: Maximilian Doré
    Host: Moa Johansson
    Grant: 1220 EUR
    Dates: 2024-03-11 to 2024-03-15

  • Initial semantics for polymorphic type systems application report
    Visitor: Benedikt Ahrens
    Host: Ambroise Lafont
    Grant: 1302 EUR
    Dates: 2024-02-04 to 2024-02-10

  • Translating from Lean to Dedukti application report
    Visitor: Rishikesh Vaishnav
    Host: Sebastian Ullrich
    Grant: 1500 EUR
    Dates: 2024-02-19 to 2024-02-25

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

6th call (8th 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 (1st 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 (1st 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 (3rd 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 (18th 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