Accepted Short-Term Scientific Missions

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

13th call (16th March 2025)

String Solving with Parametrized Automata application report
Visitor: Franziska Alber
Host: Laura Kovács
Grant: 1243 EUR
Dates: 2025-05-25 to 2025-06-01
Indexing and web search for cross libraries Proofs application
Visitor: Abdelghani Alidra
Host: Claudio Sacerdoti Coen
Grant: 1413 EUR
Dates: 2025-04-14 to 2025-04-24
Tree Transformers for Symbolic Mathematics application
Visitor: Rashid Barket
Host: François Lemaire
Grant: 966 EUR
Dates: 2025-06-30 to 2025-07-13
Formal verification of rule-based geometry application
Visitor: Pierre Boutry
Host: Vesna Marinković
Grant: 800 EUR
Dates: 2025-06-08 to 2025-06-13
The (∞,1)-category of ∞-groupoids in the spirit of Lawvere application report
Visitor: Thomas Jan Mikhail
Host: Christian Sattler
Grant: 1050 EUR
Dates: 2025-05-11 to 2025-05-24
Model Representation Formalisms for Constrained Horn Clauses over Algebraic Data Types application
Visitor: Sibylle Moehle-Rotondi
Host: Viktor Kunčak
Grant: 1189 EUR
Dates: 2025-06-16 to 2025-06-27
Informalization and Autoformalization with Dedukti and GF application report
Visitor: Aarne Ranta
Host: Frédéric Blanqui
Grant: 1548 EUR
Dates: 2025-04-09 to 2025-04-16

12th call (24th November 2024)

Verification of Higher-Order Logic Automated Reasoning within the Dedukti Framework application report
Visitor: Melanie Taprogge
Host: Alexander Steen
Grant: 1624 EUR
Dates: 2025-05-19 to 2025-05-30
Proof mining libraries for Lean application repor
Visitor: Horatiu Cheval
Host: Thomas Powell
Grant: 1716 EUR
Dates: 2025-05-11 to 2025-05-17
Dinatural Semantics of Directed Type Theory application report
Visitor: Jacob Neumann
Host: Niccolò Veltri
Grant: 1819 EUR
Dates: 2025-05-07 to 2025-05-20
Model-Checking Smart Contracts application report
Visitor: Elvis Gerardin Konjoh Selabi
Host: Alberto Lluch Lafuente
Grant: 1631 EUR
Dates: 2025-04-14 to 2025-04-25
Mapping the Landscape Between Proof Schemata and Cyclic Proofs application report
Visitor: Reuben Rowe
Host: Anela Lolić
Grant: 1677 EUR
Dates: 2025-04-06 to 2025-04-13
Designing a high-level software specification language for deductive verification application report
Visitor: Khaoula Boukir
Host: Dilian Gurov
Grant: 1580 EUR
Dates: 2025-04-05 to 2025-04-12
Algorithmic foundations of graded coalgebraic semantics application report
Visitor: Chase Ford
Host: Lutz Schröder
Grant: 1358 EUR
Dates: 2025-03-23 to 2025-03-29
Higher-Order Equational Unification and Anti-Unification for Program Verification application report
Visitor: Daniele Nantes
Host: David Cerna
Grant: 755 EUR
Dates: 2025-03-17 to 2025-03-27
From Dedukti to MMT: A Comparative Study of Modular Frameworks for Logical System application report
Visitor: Ciarán Dunne
Host: Michael Kohlhase
Grant: 1124 EUR
Dates: 2025-03-10 to 2025-03-21
Array logics and aggregation functions for program verification application report
Visitor: Roland Herrmann
Host: Dilian Gurov
Grant: 1486 EUR
Dates: 2025-03-09 to 2025-03-16
Generalization in typed languages and quantitative theories application report
Visitor: Temur Kutsia
Host: David Cerna
Grant: 600 EUR
Dates: 2025-02-23 to 2025-03-02
Adding Extensionality to Lean application
Visitor: Rishikesh Vaishnav
Host: Sebastian Ullrich
Grant: 1576 EUR
Dates: 2025-02-17 to 2025-03-02
Developing a graded type system for a resource-aware workflow modelling language application report
Visitor: Violet Ka I Pun
Host: Elena Zucca
Grant: 1520 EUR
Dates: 2025-02-16 to 2025-02-22
Translation templates for Dedukti application report
Visitor: Thomas Traversie
Host: Florian Rabe
Grant: 1530 EUR
Dates: 2025-02-02 to 2025-02-14
Modern algebraic perspectives on dualities and control effects application report
Visitor: Vikraman Choudhury
Host: Marcelo Fiore
Grant: 1131 EUR
Dates: 2025-01-28 to 2025-02-28
Initial semantics for polymorphic type systems application
Visitor: Benedikt Ahrens
Host: Ambroise Lafont
Grant: 1094 EUR
Dates: 2025-01-26 to 2025-02-01
Centralized indexing and search for LambdaPi/Dedukti Proofs application
Visitor: Claudio Sacerdoti Coen
Host: Frédéric Blanqui
Grant: 1690 EUR
Dates: 2025-01-21 to 2025-01-30
Deadlock-free context-free session types application
Visitor: Andreia Mordido
Host: Jorge A. Pérez
Grant: 1311 EUR
Dates: 2025-01-19 to 2025-01-25
Quantitative types for higher-order programming languages with effects application
Visitor: Miguel Ramos
Host: Delia Kesner
Grant: 1164 EUR
Dates: 2025-01-13 to 2025-01-22

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