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