print · source · login   

Short-Term Scientific Missions (STSMs)

Upcoming deadline for STSM applications:

    1st September 2019, for STSMs during the period  October - December 2019     

Past deadlines:

    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 79 completed STSMs, up to now, which are listed below.

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