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

9th call (17 March 2024)

  • Auditable Constraint Programming: Integrating Proof Logging with Fuzzing and Explanations application
    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
    Visitor: Jacob Neumann
    Host: Ambrus Kaposi
    Grant: 1777 EUR
    Dates: 2024-06-21 to 2024-06-29

  • Coinduction in Cubical Agda application
    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
    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
    Visitor: Oana Andrei
    Host: Dorel Lucanu
    Grant: 2131 EUR
    Dates: 2024-05-13 to 2024-05-21

8th call (7 January 2024)

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

  • Proof Theory for Programmers: Promoting Output of Theorem Provers to Formative Feedback for Computer Science Students application
    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
    Visitor: Melanie Taprogge
    Host: Frédéric Blanqui
    Grant: 2433 EUR
    Dates: 2024-03-25 to 2024-04-07

  • Bidimensional Markov categories application
    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
    Visitor: Danel Ahman
    Host: Andrej Bauer
    Grant: 2808 EUR
    Dates: 2024-02-25 to 2024-03-09

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 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
    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
    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 (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