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.

4th call (1 January 2023)

  • Translation from Dedukti to Minlog application
    Visitor: Yoan Géran (MINES ParisTech, Fontainebleau, France)
    Host: Helmut Schwichtenber (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
    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
    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
    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
    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