Short-Term Scientific Missions (STSMs)

Upcoming deadline for STSM applications:

Past deadlines:

    1st September 2019, for STSMs during the period  October - December 2019 
    1st July 2019, for STSMs during the period August - October 2019 
    5th June 2019, for STSMs during the period  15 June - August 2019
    15th February 2019, for STSMs during the period  March - April 2019
    10th January 2019 (extended) 1st January 2019, for STSMs during the period  February - April 2019
     1st October 2018, for STSMs during the period  November 2018 - February 2019
     1st July 2018, for STSMs during the period August - November 2018
    28th May 2018, for STSMs during the period June - August 2018 
    20th March 2018, for STSMs during the period  March - April 2018
    15th January 2018 (extended) 1st January 2018, for STSMs during the period  February - April 2018
    1st October 2017, for STSMs during the period  November 2017 - February 2018
    10th July 2017, for STSMs during the period August - November 2017
    15th June 2017, for STSMs during the period June - August 2017
     1st January 2017, for STSMs during the period  February - April 2017
    15th October 2016 (extended) 1st October 2016, for STSMs during the period  November 2016 - February 2017
    20th July 2016, for STSMs during the period August - November 2016

What is an STSM

A Short-Term Scientific Mission (STSM) is a research visit between countries. We encourage STSMs, as they are an effective way of starting and maintaining collaborations. It is expected that STSMs will result in publications. Remember to acknowledge the STSM funding from COST Action CA15123, and send details of the publication to the Dissemination Chair.

The coordinator for STSMs is Prof Silvia Ghilezan (University of Novi Sad, Serbia). The procedure for proposing an STSM is described in this document, and you should also read Chapter 7 of the COST Vademecum. Proposals are made through the e-COST system; the access point is here (there, click on "Actions" on the left hand side; on the new page, choose CA15123 [probably already chosen] and click on "STSM Applications" on the left hand side).

The main points about STSMs are:

• An STSM must be between two different countries which are participating in the Action.
• Multi-party STSMs are possible, i.e. several people simultaneously visiting a single host. In this case, each person who is travelling must submit a separate proposal, but the supporting documents can be shared.
• The minimum duration is 5 working days, and the maximum duration is 3 months. For early-stage researchers (less then PhD + 8 years), the maximum duration is 6 months, with approval from the Management Committee.
• The financial contribution for a STSM will be a fixed grant based on the applicant's budget request and the evaluation of the application by the STSM assessment committee. The grant will not necessarily cover all costs of the visit. The grant only covers travel and subsistence.
• Recommended (but not obligatory) grants: up to EUR 120 for daily allowance (depending on the location) and EUR 300 for travel. The total should not exceed EUR 2500 up to 3 months (or EUR 3500 for Early Stage Researchers on an STSM of longer than 3 months).
• Proposals should normally be submitted at least 6 weeks before the start of the STSM. Exceptions can be made if there is a good reason.
• Within 4 weeks of the end of the STSM, a short report must be submitted.

Prioritization:

Lower priority will be given to (in the following order of strength):

• combination visitor-host has already received funding
• visitor has already received funding
• host has already received funding for a visitor
• research group has already used many STSM opportunities (as host or visitor)

Industrial STSMs are highly rated.

List of STSMs

There were a total of 95 completed STSMs, up to now, which are listed below:

• Fourth budget period (1st May 2019 to March 2020): total 16
• Third budget period (1st May 2018 to 30th April 2019): total 30
• Second budget period (1st May 2017 to 30th April 2018): total 28
• First budget period (1st June 2016 to 30th April 2017): total 21

Fourth budget period (1st May 2019 to March 2020): total up to now 16

• Categorical structures for type theory in univalent foundations - Part II
  Visitor: Benedikt Ahrens (INRIA, Nantes, FR)
  Host: Peter Lumsdaine (Stockholm University, SE)
  Dates: 2019-09-29 to 2019-10-05
  Outcome: abstract at TYPES2020
• Modal Lambda-Calculi and Translations
  Visitor: Tarmo Uustalu (Tallinn University of Technology, EE)
  Host: Luís Pinto (University of Minho, PT)
  Dates: 2019-10-17 to 2019-10-26
  Outcome: abstract at TYPES2020
• Canonicity for Homotopy Type Theory with Propositional Identity Types
  Visitor: Martijn Den Besten (University of Amsterdam, NL)
  Host: Erik Palmgren (Stockholm University, Sweden)
  Dates: 2019-10-13 to 2019-11-09
• Free Algebras, Presentations of Monads and Final Coalgebras in HoTT
  Visitor: Niccolo Veltri (Tallinn University of Technology, EE)
  Host: Henning Basold (University Leiden, NL)
  Dates: 2019-11-18 to 2019-11-26
  Outcome: abstract at TYPES2020
• Proof Construction in HOL
  Visitor: Gergely Buday ( Károly Róbert Campus, Gyöngyös, HU)
  Host: Magnus Myreen (Chalmers University, Sweden)
  Dates: 2019-11-04 to 2019-11-08
• Call-by-push-value and polarities
  Visitor: José Espírito Santo (University of Minho, PT)
  Host: Delia Kesner (Université Paris Diderot - Paris 7, FR)
  Dates: 2019-10-27 to 2019-11-01
• Semantics and Extensions of Sized Inductive-Coinductive Types
  Visitor: Henning Basold (Leiden University, NL)
  Host: Ekaterina Komendantskaya (Heriot-Watt University, UK)
  Dates: 2019-08-04 to 2019-08-10
• Algebraic effects for Software Transactional Memory
  Visitor: Marino Miculan (University of Udine, IT)
  Host: Tarmo Uustalu (Tallinn University of Technology, EE)
  Dates: 2019-09-08 to 2019-09-14
• Initiality of Inductive-Inductive Types
  Visitor: Jakob von Raumer (University of Nottingham, UK)
  Host: Ambrus Kaposi (Eotvos Lorand University, Budapest, Hungary)
  Dates: 2019-08-01 to 2019-08-31
  Outcome paper at FSCD2020
• Concurrent Abstract Machines
  Visitor: Sergueï Lenglet (Universite de Lorraine, FR)
  Host: Dariusz Biernacki (University of Wroclaw, PL)
  Dates: 2019-09-16 to 2019-09-20
• Concurrent Abstract Machines
  Visitor: Alan Schmitt (Inria Bretagne Atlantique, Rennes, FR)
  Host: Dariusz Biernacki (University of Wroclaw, PL)
  Dates: 2019-09-16 to 2019-09-20
• Type Theoretical Formalism of Argumentative Functionality Indicators
  Visitor: Matthaios Bournazos (National Technical University of Athens, Greece)
  Host: Silvia Ghilezan (University of Novi Sad, Serbia)
  Dates: 2019-09-09 to 2019-09-13
• Importing Agda proofs in Logipedia
  Visitor: Guillaume Genestier ( ENS Paris-Saclay, FR)
  Host: Andreas Abel (Chalmers University, Sweden)
  Dates: 2019-07-07 to 2019-08-10
• Scalable programming with multi-shot handlers
  Visitor: Matija Pretnar (University of Ljubljana, Slovenia)
  Host: Sam Lindley (University of Edinburgh, UK)
  Dates: 2019-06-26 to 2019-07-17
• Bicategories in Univalent Foundations and the Rezk Completion
  Visitor: Niccolo Veltri (IT University of Copenhagen, DK)
  Host: Marco Maggesi (University of Florence, IT)
  Dates: 2019-07-22 to 2019-07-26
  Outcome: submitted paper
• Bicategories in Univalent Foundations and the Rezk Completion
  Visitor: Niels van der Weide (Radboud University, Nijmegen, NL)
  Host: Marco Maggesi (University of Florence, IT)
  Dates: 2019-07-22 to 2019-07-26
  Outcome: submitted paper

Third budget period (1st May 2018 to 30th April 2019): total up to now 30

• Using behavioral types for verifying communication correctness in the Scilla language
  Visitor: Radu Ometita (Faculty of Informatics, Iasi, Romania)
  Host: Jorge Pérez (University of Groningen, NL)
  Dates: 2019-04-01 to 2019-04-05
• A general definition of cubical type theories
  Visitor: Philipp Haselwarter (University of Ljubljana, Slovenia)
  Host: Bas Spitters (Aarhus University, DK)
  Dates: 2019-04-14 - 2019-04-28
• Multi-Language Semantics in Iris
  Visitor: Jonas Kastberg Hinrichse (IT University of Copenhagen, DK)
  Host: Robbert Krebbers (TU Delft, NL)
  Dates: 2019-04-11 - 2019-04-19
  Outcome: paper at POPL2020
• Proving canonicity for Setoid type theory
  Visitor: Simon Boulier (NRIA (Nantes), FR)
  Host: Ambrus Kaposi (Eotvos Lorand University, Budapest, Hungary)
  Dates: 2019-03-05 - 2019-03-22
  Outcome: paper at MPC 2019
• Behavioural Aggregate Computing for the Internet of Things
  Visitor: Violet Ka I Pun (Western Norway University of Applied Sciences, NO)
  Host: Ferruccio Damiani (University of Torino, IT)
  Dates: 2019-04-10 - 2019-04-17
• A Uniform Framework for Governed Multiparty Session Semanitics
  Visitor: Nobuko Yoshida (Imperial College London, UK)
  Host: Dimitrios Kouzapas (University of Cyprus, CY)
  Dates: 2019-04-16 - 2019-04-25
• Eff-Bayes: a modular Bayesian inference library with algebraic effects and handlers
  Visitor: Ohad Kammar (University of Edinburgh, UK)
  Host: Matija Pretnar (University of Ljubljana, Slovenia)
  Dates: 2019-02-09 to 2019-02-20
  Outcome: seminar at KAIST in South Korea
• Probabilistic reasoning in lambda calculus
  Visitor: Simona Kasterovic (University of Novi Sad, RS)
  Host: Alex Simpson (University of Ljubljana, Slovenia)
  Dates: 2019-03-23 to 2019-03-30
• Efficient type checking in proof assistants
  Visitor: Andrea Condoluci (Universita' di Bologna, IT)
  Host: Beniamino Accattoli (INRIA Saclay, FR)
  Dates: 2019-01-14 to 2019-02-28
  Outcome: paper at PPDP 2019
• Meta-theorems about general type theories
  Visitor: Andrej Bauer (University of Ljubljana, Slovenia)
  Host: Peter Lumsdaine (Stockholm University, Sweden)
  Dates: 2019-02-01 to 2019-02-07
• Better Late Than Never: A Fully Abstract Semantics for Classical Processes
  Visitor: Wen Kokke (University of Edinburgh, UK)
  Host: Fabrizio Montesi (University of Southern Denmark, DK)
  Dates: 2019-03-01 to 2019-04-30
• Type theory with custom rewrite rules: confluence checking & applications
  Visitor: Jesper Cockx (University of Gothenburg, Sweden)
  Host: Nicolas Tabareau (Inria Rennes-Bretagne Atlantique, FR)
  Dates: 2019-01-28 to 2019-02-08
• Bicategories in Homotopy Type Theory
  Visitor: Daniil Frumin (Radboud University, NL)
  Host: Marco Maggesi (University of Florence, IT)
  Dates: 2018-11-26 to 2018-11-30
  Outcomes: UniMath formalisation, paper at FSCD 2019
• Reinforcing ENIGMA Guidance with Reinforcement Learning
  Visitor: Jan Jakubuv (Chech Technical University Prague, Czech Republic)
  Host: Cezary Kaliszyk (University of Innsbruck, AT)
  Dates: 2018-11-19 to 2018-12-14
• Deep learning techniques for automated theorem proving
  Visitor: Bartosz Piotrowski (University of Warsaw, PL)
  Host: Cezary Kaliszyk (University of Innsbruck, AT)
  Dates: 2018-11-12 to 2018-11-30
  Outcome: paper at ICML 2019
• Bicategories in Homotopy Type Theory
  Visitor: Niels van der Weide (Radboud University, Nijmegen, NL)
  Host: Marco Maggesi (University of Florence, IT)
  Dates: 2018-11-26 to 2018-11-30
  Outcomes: UniMath formalisation, paper at FSCD 2019
• Bicategories
  Visitor: Benedikt Ahrens (University of Birmingham, UK)
  Host: Marco Maggesi (University of Florence, IT)
  Dates: 2018-11-25 to 2018-12-01
  Outcome: paper at FSCD 2019
• Constructing Inductive-Inductive Types
  Visitor: Jakob von Raumer (University of Nottingham, UK)
  Host: Ambrus Kaposi (Eotvos Lorand University, Budapest, Hungary)
  Dates: 2019-01-11 to 2019-01-27
  Outcome: abstract at TYPES 2019
• Step-indexed logical relations for Dependent Object Types
  Visitor: Paolo Giosué Giarrusso (EPFL Laussane, CH)
  Host: Lars Birkedal (Aarhus University, DK)
  Dates: 2018-10-29 to 2018-11-02
• A general meta-theory of dependent type theories
  Visitor: Peter Lumsdaine (Stockholm University, Sweden)
  Host: Andrej Bauer (University of Ljubljana, Slovenia)
  Dates: 2018-11-06 to 2018-11-13
• Lambda calculi with a comonad
  Visitor: José Espírito Santo (University of Minho, PT)
  Host: Tarmo Uustalu (Tallinn University of Technology, EE)
  Dates: 2018-09-30 to 2018-10-06
  Outcome: paper at FSCD 2019
• Precise subtyping for interleaved multiparty sessions
  Visitor: Nobuko Yoshida (Imperial College London, UK)
  Host: Silvia Ghilezan (University of Novi Sad, Serbia)
  Dates: 2018-09-13 to 2018-09-22
  Outcomes: paper at POPL 2019, paper in JLAMP
• Lambda calculi with a comonad
  Visitor: Luís Pinto (University of Minho, PT)
  Host: Tarmo Uustalu (Tallinn University of Technology, EE)
  Dates: 2018-09-30 to 2018-10-06
  Outcome: paper at FSCD 2019
• Higher order view shift specifications and logically atomic specifications
  Visitor: Daniil Frumin (Radboud University, NL)
  Host: Lars Birkedal (Aarhus University, DK)
  Dates: 2018-07-31 to 2018-08-14
  Outcome: paper at Security & Privacy 2021
• Abstraction in Idris for Sequential Decision Problems
  Visitor: Edwin Brady (University of St Andrews, UK)
  Host: Nicola Botta (ETH Zurich, CH)
  Dates: 2018-09-16 to 2018-09-29
• From Abstract Machines to Other Semantic Artifacts and Back
  Visitor: Sergueï Lenglet (Universite de Lorraine, FR)
  Host: Dariusz Biernacki (University of Wroclaw, PL)
  Dates: 2018-11-12 to 2018-11-16
  Outcomes: paper at FOSSACS 2019, paper at MFPS 2019
• Precise subtyping for interleaved multiparty sessions
  Visitor: Alceste Scalas (Imperial College London, UK)
  Host: Silvia Ghilezan (University of Novi Sad, Serbia)
  Dates: 2018-09-13 to 2018-09-22
  Outcome: paper at POPL 2019
• From Abstract Machines to Other Semantic Artifacts and Back
  Visitor: Alan Schmitt (Inria Bretagne Atlantique, Rennes, FR)
  Host: Dariusz Biernacki (University of Wroclaw, PL)
  Dates: 2018-11-12 to 2018-11-16
  Outcomes: paper at FOSSACS 2019, paper at MFPS 2019
• Using "behavioural types" and "syntactic models of imperative calculi" in the formalization and analysis of reliable systems
  Visitor: Paola Giannini (Universita del Piemonte Orientale, IT)
  Host: Violet Ka I Pun (Western Norway University of Applied Sciences, NO)
  Dates: 2018-08-06 to 2018-08-20
• Formalization of the sequent calculus' meta-theory
  Visitor: Matthias Puech (CNAM, FR)
  Host: José Espírito Santo (University of Minho, PT)
  Dates: 2018-07-16 to 2018-07-20

Second budget period (1st May 2017 to 30th April 2018): total up to now 28

• A meta-theory of type theories -- formalization of type theories over a signature
  Visitor: Philipp Haselwarter (University of Ljubljana, Slovenia)
  Host: Peter Lumsdaine (Stockholm University, Sweden)
  Dates: 2018-04-23 to 2018-04-30
• Initial syntax for dependent type theories
  Visitor: Benedikt Ahrens (University of Birmingham, UK)
  Host: Marco Maggesi (University of Florence, IT)
  Dates: 2018-04-22 to 2018-04-28
  Outcome: paper at FSCD 2019
• Semantics and Extensions of Sized Inductive-Coinductive Types
  Visitor: Henning Basold (ENS Lyon, FR)
  Host: Herman Geuvers (Radboud University, NL)
  Dates: 2018-04-18 to 2018-04-25
• Categorical Models of Derivations in Theories with Non-Logical Axioms
  Visitor: Serguei Solovyev (Paul Sabatier University, Toulouse, FR)
  Host: Sara Negri, (University of Helsinki, Finland)
  Dates: 2018-04-12 to 2018-04-25
• Relational verification of light-weight concurrency
  Visitor: Amin Timany (KU Leuven, Belgium)
  Host: Lars Birkedal (Aarhus University, DK)
  Dates: 2018-04-09 to 2018-04-13
  Outcomes: Link to POPL paper
• Predicative semantics for sized dependent types
  Visitor: Andreas Abel (Chalmer/Gothenburg University, Sweden)
  Host: Herman Geuvers (Radboud University, NL)
  Dates: 2018-04-08 to 2018-04-14
• Relational verification of a MPMC queue datastructure in Coq
  Visitor: Daniil Frumin (Radboud University, NL)
  Host: Lars Birkedal (Aarhus University, DK)
  Dates: 2018-04-08 to 2018-04-14
  Outcomes: Link to LICS paper
• Rational Causality
  Visitor: Jurriaan Rot (Radboud University, NL)
  Host: Stefan Milius (Friedrich-Alexander Universität Erlangen-Nürnberg, DE)
  Dates: 2018-04-08 to 2018-04-13
• Study of machine-learning techniques over formal mathematics in Mizar
  Visitor: Adam Naumowicz (University of Bialystok, PL)
  Host: Josef Urban (Czech Technical University in Prague, CZ)
  Dates: 2017-04-08 to 2017-04-14
  Outcome: paper at CICM 2018
• A meta-theory of type theories: models and interpretations
  Visitor: Peter Lumsdaine (Stockholm University, Sweden)
  Host: Andrej Bauer (University of Ljubljana, Slovenia)
  Dates: 2018-03-29 to 2018-04-03
• Type-based parallel programming
  Visitor: Atanas Hristov (University Ohrid, FYR Macedonia)
  Host: Anastasios Panagiotis (Aristotle University of Thessaloniki, GR)
  Dates: 2018-03-19 to 2018-04-16
• Fully-abstract compilation between capability machines
  Visitor: Lau Skorstengaard (Aarhus University, Aarhus, DK)
  Host: Dominique Devriese (KU Leuven, BE)
  Dates: 2018-03-18 to 2018-03-23
  Outcomes: Link to PLS paper
• Construction of Higher Inductive Types
  Visitor: Niels van der Weide (Radboud University, NL)
  Host: Andrej Bauer (University of Ljubljana, Slovenia)
  Dates: 2018-03-05 to 2018-03-16
  Outcomes: formalisation, paper at MFPS
• A cubical sets model for a 2-level type theory with fibrant replacement
  Visitor: Simon Huber (University of Gothenburg, SE)
  Host: Nicolas Tabareau (École des Mines de Nantes, FR)
  Dates: 2018-02-25 to 2018-03-03
• Extending definitional proof irrelevance with inductive datatypes
  Visitor: Jesper Cockx (University of Gothenburg, SE)
  Host: Nicolas Tabareau (École des Mines de Nantes, FR)
  Dates: 2018-02-19 to 2018-02-23
• Verification of Relaxed Memory Programs
  Visitor: Hendrik Maarand (Tallinn University of Technology, EE)
  Host: Georg Struth (University of Sheffield, UK)
  Dates: 2018-02-18 to 2018-02-23
• Developing Cubical Type Theory
  Visitor: Andrea Vezzosi (Chalmers University, SE)
  Host: Conor McBride (University of Strathclyde, UK)
  Dates: 2018-02-04 to 2018-03-25
• Initial syntax for dependent type theories
  Visitor: Marco Maggesi (University of Florence, IT)
  Host: Benedikt Ahrens (University of Birmingham, UK)
  Dates: 2018-02-15 to 2018-03-01
  Outcome: paper at FSCD 2019
• Learning to Reason with Coq Tactics
  Visitor: Lasse Blaauwbroek (Chez Institute of Informatics, CZ)
  Host: Cezary Kaliszik (University of Innsbruck, AT)
  Dates: 2018-02-01 to 2018-03-02
• Towards a logical framework with intersection and union types
  Visitor: Luigi Liquori (INRIA Sophia Antipolis, FR)
  Host: Furio Honsell (University of Udine, IT)
  Dates: 2018-01-21 to 2018-02-01
  Outcomes: paper in MSCS, paper at FSCD 2019, paper at FSTTCS 2018
• Probabilistic Session Types and their Semantics
  Visitor: Simon Castellan (Imperial College London, UK)
  Host: Jorge Pérez (University of Groningen, NL)
  Dates: 2018-01-07 to 2018-01-14
• Probabilistic Session Types and their Semantics
  Visitor: Nobuko Yoshida (Imperial College London, UK)
  Host: Jorge Pérez (University of Groningen, NL)
  Dates: 2018-01-07 to 2018-01-14
• AI Methods for Hardening Type Theory Hammers
  Visitor: Jan Jakubuv (Czech Technical University Prague, CZ)
  Host: Cezary Kaliszyk (University of Innsbruck, AT)
  Dates: 2017-11-20 to 2017-12-15
  Outcomes: Link to ICMS paper
• Foundations of Semantic Types and Related Systems for Program Synthesis and Proofs
  Visitor: Andrej Dudenhefner (Technical University of Dortmund, DE)
  Host: Ugo de'Liguoro (Università di Torino, IT)
  Dates: 2017-09-21 to 2017-09-27
  Outcomes: Link to LMCS paper
• Model theory of semantic types
  Visitor: Boris Duedder (Technical University Copenhagen, DK)
  Host: Ugo de'Liguoro (Università di Torino, IT)
  Dates: 2017-09-20 to 2017-09-26
  Outcomes: Link to LMCS paper
• Formalisation of a C-like imperative language and logical relations in Iris
  Visitor: Daniil Frumin (Radboud University, Nijmegen, NL)
  Host: Lars Birkedal (Aarhus University, DK)
  Dates: 2017-08-31 to 2017-11-07
  Outcomes: Link to LICS paper
• Setoid type theory
  Visitor: Ambrus Kaposi (Eötvös Loránd University, HU)
  Host: Nicolas Tabareau (École des Mines de Nantes, FR)
  Dates: 2017-08-28 to 2017-09-01
  Outcome: paper at MPC 2019
• Mechanized separation logic proofs in Coq
  Visitor: Robbert Krebbers (TU Delft, NL)
  Host: Lars Birkedal (Aarhus University, DK)
  Dates: 2017-08-20 to 2017-08-26

First budget period (1st June 2016 to 30th April 2017): total 21

• Display map categories for models of type theory
  Visitor: Benedikt Ahrens (INRIA, Nantes, FR)
  Host: Peter Lumsdaine (Stockholm University, SE)
  Dates: 2017-04-04 to 2017-04-17
  Outcome: LMCS paper
• Concurrency, abstract machines, and control operators
  Visitor: Sergueï Lenglet (INRIA Bretagne Atlantique, Rennes, FR)
  Host: Dariusz Biernacki (University of Wroclaw, PL)
  Dates: 2017-04-03 to 2017-04-08
  Outcomes: paper at LICS 2017, paper at MFPS 2017
• Concurrency, abstract machines, and control operators
  Visitor: Alan Schmitt (INRIA Bretagne Atlantique, Rennes, FR)
  Host: Dariusz Biernacki (University of Wroclaw, PL)
  Dates: 2017-04-03 to 2017-04-08
  Outcomes: paper at LICS 2017, paper at MFPS 2017
• Object-Oriented Programming in Dependent Type Theory - Inheritance, Heap, Case Studies
  Visitor: Stephan Adelsberger (Vienna University of Economics and Business, Vienna, AT)
  Host: Anton Setzer (Swansea University, Swansea, UK)
  Dates: 2017-04-02 to 2017-04-15
  Outcomes: Link to JFP paper
• Precise asynchronous subtyping for multiparty session types
  Visitor: Alceste Scalas (Imperial College London, UK)
  Host: Silvia Ghilezan (University of Novi Sad, RS)
  Dates: 2017-03-21 to 2017-03-28
  Outcome: JLAMP paper
• Precise asynchronous subtyping for multiparty session types
  Visitor: Nobuko Yoshida (Imperial College London, UK)
  Host: Silvia Ghilezan (University of Novi Sad, RS)
  Dates: 2017-03-21 to 2017-03-28
  Outcomes: JLAMP paper
• Automation in typed proof assistants
  Visitor: Thibault Gauthier (University of Innsbruck, AT)
  Host: Josef Urban (Czech Institute of of Informatics, Robotics and Cybernetics, Prague, CZ)
  Dates: 2017-01-30 to 2017-03-03
• Applications of Dependent Types to Hardware Design and Verification
  Visitor: João Paulo Pizani Flor (Utrecht University, NL)
  Host: Mary Sheeran (Chalmers University of Technology, Gothenburg, SE)
  Dates: 2017-02-20 to 2017-04-02
  Outcomes: Link to ITP paper
• Real Numbers and Homotopy Type Theory
  Visitor: Niels van der Weide (Radboud University, Nijmegen, NL)
  Host: Andrej Bauer (University of Ljubljana, Slovenia)
  Dates: 2017-01-29 to 2017-02-19
  Outcome: talk at FPFM 2017
• Lambda-calculi with a comonad
  Visitor: Tarmo Uustalu, (Institute of Cybernetics at TUT, Tallinn, EE)
  Host: José Espírito Santo (University of Minho, Braga, PT)
  Dates: 2016-12-12 to 2016-12-17
  Outcome: paper at FSCD 2019
• Types, Verification and Privacy
  Visitor: Petros Stefaneas (National Technical University of Athens, GR)
  Host: Silvia Ghilezan (University of Novi Sad, RS)
  Dates: 2017-01-22 to 2017-01-27
• Translations between type theories with univalence
  Visitor: Robin Adams (Universitetet i Bergen, NO)
  Host: Thierry Coquand (University of Gothenburg, SE)
  Dates: 2016-11-12 to 2016-11-19
  Outcome: paper in TYPES 2016 post-proceedings
• Normalisation by Evaluation for dependent types
  Visitor: Ambrus Kaposi (Eötvös Loránd University, Budapest, HU)
  Host: Thorsten Altenkirch (University of Nottingham, UK)
  Dates: 2016-11-23 to 2016-12-01
  Outcome: paper in LMCS
• Intersection types for sequent calculus
  Visitor: José Espírito Santo (University of Minho, Braga, PT)
  Host: Silvia Ghilezan (University of Novi Sad, RS)
  Dates: 2016-10-23 to 2016-10-29
  Outcomes: Link to PPDP paper
• Model theory for Combinatory Logic with Intersection Types
  Visitor: Andrej Dudenhefner (Technical University of Dortmund, DE)
  Host: Ugo de'Liguoro (Universita di Torino, IT)
  Dates: 2016-09-25 to 2016-10-01
  Outcomes: Link to LMCS paper
• Model theory for Combinatory Logic with Intersection Types
  Visitor: Boris Duedder (Technical University of Dortmund, DE)
  Host: Ugo de'Liguoro (Universita di Torino, IT)
  Dates: 2016-09-25 to 2016-10-01
  Outcomes: Link to LMCS paper
• Logical Relations for effectful programming languages
  Visitor: Amin Timany (KU Leuven, BE)
  Host: Lars Birkedal (Aarhus University, DK)
  Dates: 2016-08-15 to 2016-11-13
• Dependently Typed Version Control system
  Visitor: Victor Miraldo (University of Utrecht, NL)
  Host: Pierre Evariste Dagand (LIP6, Paris, FR)
  Dates: 2016-10-06 to 2016-10-15
• Event semantics and coercive subtyping
  Visitor: Serguei Solovyev (Paul Sabatiér University (Toulouse-3), FR)
  Host: Zhaohui Luo, Royal Holloway (University of London, UK)
  Dates: 2016-09-14 to 2016-09-20
  Outcomes: Link to WoLLIC paper
• Formalisation of the metatheory of type theory
  Visitor: Peter Lumsdaine (Stockholm University, SE)
  Host: Andrej Bauer (University of Ljubljana, Slovenia)
  Dates: 2016-11-20 to 2016-11-30
• Reasoning About Capability Systems using Logical Relations
  Visitor: Lau Skorstengaard (Aarhus University, Aarhus, DK)
  Host: Dominique Devriese (KU Leuven, BE)
  Dates: 2016-10-23 to 2016-12-16
  Outcomes: Link to POPL paper