European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST H2020 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.

3rd call (1 July 2022)

  • Behavioural Types for Smart Contracts
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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