23rd International Conference on
Types for Proofs and Programs,

TYPES 2017

Budapest, Hungary, 29 May - 1 June 2017



Budapest   Tram   Budapest Panorama HDR


     

PHOTOS

BACKGROUND

The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming.

The meetings from 1990 to 2008 were annual workshops of a sequence of five EU funded networking projects. Since 2009, TYPES has been run as an independent conference series. Previous TYPES meetings were held in Antibes (1990), Edinburgh (1991), Båstad (1992), Nijmegen (1993), Båstad (1994), Torino (1995), Aussois (1996), Kloster Irsee (1998), Lökeberg (1999), Durham (2000), Berg en Dal near Nijmegen (2002), Torino (2003), Jouy-en-Josas near Paris (2004), Nottingham (2006), Cividale del Friuli (2007), Torino (2008), Aussois (2009), Warsaw (2010), Bergen (2011), Toulouse (2013), Paris (2014), Tallinn (2015), Novi Sad (2016).

The TYPES areas of interest include, but are not limited to:

  • foundations of type theory and constructive mathematics;
  • applications of type theory;
  • dependently typed programming;
  • industrial uses of type theory technology;
  • meta-theoretic studies of type systems;
  • proof assistants and proof technology;
  • automation in computer-assisted reasoning;
  • links between type theory and functional programming;
  • formalizing mathematics using type theory.


We encourage talks proposing new ways of applying type theory. In the spirit of workshops, talks may be based on newly published papers, work submitted for publication, but also work in progress.

FINANCIAL SUPPORT

The first two days of TYPES 2017, May 29 - 30 are organised by EUTypes Cost Action CA15123. On May 30 there will be an EUTypes Management Committee (MC) meeting, and on both days there will be WG meetings. This means that members of the EUTypes MC will be invited for these 2 days through the e-cost system, and their cost of travel and stay will be covered. There will likely be some funding for a limited number of other invited speakers. The funding is subject to COST rules, and invitations will be sent out via the e-cost system after the 1st of May.



INVITED SPEAKERS

thumb
EDWIN BRADY

University of St Andrews

An Architecture for Dependently Typed Applications in Idris

A useful pattern in dependently typed programming is to define a state transition system, for example the states and operations in a network protocol, as an indexed monad. We index each operation by its input and output states, thus guaranteeing that operations satisfy pre- and post-conditions, by typechecking. However, what if we want to write a program using several systems at once? What if we want to define a high level state transition system, such as a network application protocol, in terms of lower level states, such as network sockets and mutable variables?

In this talk, I will present an architecture for dependently typed applications in the Idris programming language, based on a hierarchy of state transition systems, and implemented in a generic data type ST. This is based on a monad indexed by contexts of resources, allowing us to reason about multiple state transition systems in the type of a function. Using ST, I will show: how to implement a state transition system as a dependent type, with type level guarantees on its operations; how to account for operations which could fail; how to combine state transition systems into a larger system; and, how to implement larger systems as a hierarchy of state transition systems. I will illustrate the system with a high level network application protocol, implemented in terms of POSIX network sockets.

thumb
SARA NEGRI

University of Helsinki

Proof systems based on neighbourhood semantics

A method is presented for generating proof systems on the basis of neighbourhood semantics. The method is a generalisation of the internalisation of possible worlds semantics into sequent calculi. Its specific features will be illustrated through case studies from the treatment of counterfactuals and conditional beliefs.

THIS TALK IS CANCELLED.

thumb
JAKOB REHOF

TU Dortmund

Bounding Principles for Decision Problems with Intersection Types

The classical type-theoretic decision problems, inhabitation (given a type, is there a term having the type?) and typability (given a term, does it have a type?), are undecidable for intersection types. But one can consider bounding principles admitting of algorithmic solutions while retaining interesting levels of expressive power. We overview the status of known bounding principles, computational aspects of the associated decision problems, and some application perspectives.

CONTRIBUTED TALKS

We solicit contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pp formatted with easychair.cls. The submission site is https://easychair.org/conferences/?conf=types2017.

Important dates:

  • submission of 2 pp abstract: 20 March 2017
  • notified of acceptance/rejection: 17 April 2017
  • camera-ready version of abstract: 12 May 2017

When preparing the final versions, please:

  • don't upload copyright transfer form
  • include easychair.cls and all files necessary for LaTeX compilation in the zip file

Camera-ready versions of the accepted contributions will be published in an informal book of abstracts for distribution at the workshop.

Accepted papers:

The conference proceedings can be downloaded.

Talks last 15 minutes followed by 5 minutes question time. You can find the slides for the uploaded talks here: https://www.dropbox.com/sh/unwi307a12pwyuh/AACtRaRU1Hlb1CbldGbqitf9a?dl=0.



POST-PROCEEDINGS

Open call for papers

TYPES is a major forum for the presentation of research on all aspects of type theory and its applications. TYPES 2017 was held between 29 May and 1 June in Budapest, Hungary. The post-proceedings volume will be published in LIPIcs, Leibniz International Proceedings in Informatics, an open-access series of conference proceedings.

Submission to this post-proceedings volume is open to everyone, also to those who did not participate in the conference.

We would like to invite all researchers that study and apply type systems to share their results. In particular, we welcome submissions on the following topics:

  • Foundations of type theory and constructive mathematics;
  • Homotopy type theory;
  • Applications of type theory;
  • Dependently typed programming;
  • Industrial uses of type theory technology;
  • Meta-theoretic studies of type systems;
  • Proof assistants and proof technology;
  • Automation in computer-assisted reasoning;
  • Links between type theory and functional programming;
  • Formalizing mathematics using type theory;
  • Type theory in linguistics.

Important dates:

  • Abstract submission: 16 October 2017
  • Paper submission: 23 October 2017
  • Author notification: 26 March 2018

Details:

  • Papers have to be formatted with lipics.cls and adhere to the style requirements of LIPIcs.
  • The recommended length of a paper is 15-25 pages. Submissions significantly longer than 25 pages will not be considered.
  • Papers have to be submitted in pdf through EasyChair: https://easychair.org/conferences/?conf=types2017postproceed
  • Authors have the option to attach to their submission a zip or tgz file containing code (formalized proofs or programs), but reviewers are not obliged to take those attachments into account and they will not be published.
  • In case of questions, please contact one of the editors.

Editors:

REGISTRATION

Registration for the conference is open at https://e-conf.com/eutypes2017/registration.

Registration fees:

Early bird (before 10 May)Normal (after 10 May)
Normal participant250 EUR300 EUR
Student200 EUR250 EUR
Registration for only the first two days
of the conference (COST MC meeting)
170 EUR220 EUR

The registration fee for participants and students includes:

  • Book of proceedings
  • Daily lunches
  • Coffee breaks
  • Conference dinner

The registration fee for COST MC participants who only come for the first two days includes:

  • Book of proceedings
  • Daily lunches
  • Coffee breaks

We strongly recommend registering for the excursion because it is a great opportunity for discussion of research ideas in a relaxed environment and for general networking.

Ticket for excursion on 30 May (not included in registration fee)30 EUR
Extra ticket for conference dinner on 31 May50 EUR

Cancelling registration: if registration is cancelled, full refund is guaranteed until 10 May, 50% refund until 15 May.



PROGRAMME

Program overview

Talks last 15 minutes followed by 5 minutes question time. You can find the slides for the uploaded talks here: https://www.dropbox.com/sh/unwi307a12pwyuh/AACtRaRU1Hlb1CbldGbqitf9a?dl=0.

29 May (Monday)
(EUTypes meeting)
30 May (Tuesday)
(EUTypes meeting)
31 May (Wednesday)1 June (Thursday)
8.30-9.00registration
9.00-10.00session 1 (3 talks)invited talk: Jakob Rehofsession 8 (3 talks)invited talk: Edwin Brady
10.00-10.20coffee breakcoffee breakcoffee breakcoffee break
10.20-11.20session 2 (3 talks)session 6 (3 talks)session 9 (3 talks)session 14 (3 talks)
11.20-11.40coffee breakcoffee breakcoffee breakcoffee break
11.40-12.40session 3 (3 talks)session 7 (3 talks)session 10 (3 talks)session 15 (3 talks)
12.40-14.20lunchlunch (until 14.00)lunchlunch
14.20-16.00session 4 (3 talks) + WG meetingsMC meeting + business meeting (14.00-15.30)session 11 (5 talks)session 16 (5 talks)
16.00-16.30coffee breakexcursion (15.30-20.00)coffee breakcoffee break
16.30-18.10WG + dissemination meetings (until 17.00)session 12 (5 talks)session 17 (2 talks) (until 17.40)
18.40-conference dinner

29 May (Monday) (EUTypes meeting)

8.30-9.00registration
9.00-9.20Session 1 (chair: Ambrus Kaposi)Thomas Winant, Jesper Cockx and Dominique Devriese. Expressive and Strongly Type-Safe Code Generation
9.20-9.40Nils Anders Danielsson and Víctor López Juan. Towards practical out-of-order unification
9.40-10.00Guillaume Allais. Typing with Leftovers: a Mechanisation of ILL
10.00-10.20coffee break
10.20-10.40Session 2 (chair: Silvia Ghilezan)Bogdan Aman and Gabriel Ciobanu. A Probabilistic Approach of Behavioural Types
10.40-11.00Frederic Gilbert. Verifiable certificates for predicate subtyping
11.00-11.20Luigi Liquori and Claude Stolze. Intersection and Union Types from a Proof-functional Point of View
11.20-11.40coffee break
11.40-12.00Session 3 (chair: Tarmo Uustalu)Branislava Živković and Milena Vujosevic Janicic. Parallelization of Software Verification Tool LAV
12.00-12.20Adam Naumowicz. Adjective Clustering in the Mizar Type System
12.20-12.40Andrej Bauer, Philipp G. Haselwarter and Théo Winterhalter. A modular formalization of type theory in Coq
12.40-14.20lunch
14.20-14.40Session 4 (chair: Andreas Abel)Benedikt Ahrens, Ralph Matthes and Anders Mörtberg. Monads from multi-sorted binding signatures
14.40-15.00Francisco Ferreira, David Thibodeau and Brigitte Pientka. Dependent Type Theory with Contextual Types
15.00-15.20G. A. Kavvos. A Type-Theoretic Alternative to LISP
15.20-16.00EUTypes WG meetings (open to any conference participant)
16.00-16.30coffee break
16.30-17.00EUTypes WG and dissemination meetings (open to any conference participant)

30 May (Tuesday) (EUTypes meeting)

9.00-10.00Session 5 (chair: Aleksy Schubert)INVITED TALK: Jakob Rehof. Bounding Principles for Decision Problems with Intersection Types
10.00-10.20coffee break
10.20-10.40Session 6 (chair: Fredrik Nordvall Forsberg)Aleš Bizjak and Rasmus Ejlers Møgelberg. Presheaf semantics for guarded dependent type theory
10.40-11.00Andreas Abel, Andrea Vezzosi and Théo Winterhalter. Normalization by Evaluation for Sized Dependent Types
11.00-11.20Thorsten Altenkirch, Ambrus Kaposi and András Kovács. Normalisation by Evaluation for a Type Theory with Large Elimination
11.20-11.40coffee break
11.40-12.00Session 7 (chair: Hugo Herbelin)Thierry Coquand, Bassel Mannaa and Fabian Ruch. A Model of Type Theory in Stacks
12.00-12.20Pierre-Marie Pédrot and Nicolas Tabareau. An Effectful Way to Eliminate Addiction to Dependence
12.20-12.40Valentin Blot. An interpretation of system F through bar recursion
12.40-14.00lunch
14.00-15.00EUTypes MC meeting (open to any conference participant)
15.00-15.30TYPES conference business meeting
15.30-20.00excursion

31 May (Wednesday)

9.00-9.20Session 8 (chair: Pierre-Marie Pédrot)Patrick Bahr, Hans Bugge Grathwohl and Rasmus Ejlers Møgelberg. The Clocks Are Ticking: No More Delays! Reduction Semantics for Type Theory with Guarded Recursion
9.20-9.40Gilles Dowek, Jean-Pierre Jouannaud, Assaf Ali and Jiaxiang Liu. Untyped Confluence In Dependent Type Theories
9.40-10.00Stefan Ciobaca and Vlad Andrei Tudose. Automatically Constructing a Type System from the Small-Steps Semantics
10.00-10.20coffee break
10.20-10.40Session 9 (chair: Anton Setzer)Andrej Dudenhefner and Jakob Rehof. Lower End of the Linial-Post Spectrum
10.40-11.00José Espírito Santo, Ralph Matthes and Luís Pinto. Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search
11.00-11.20David Baelde, Amina Doumane, Guilhem Jaber and Alexis Saurin. Bouncing threads for infinitary proof theory
11.20-11.40coffee break
11.40-12.00Session 10 (chair: Matthieu Sozeau)Jose Espirito Santo and Silvia Ghilezan. Characterization of strong normalizability for a lambda-calculus with co-control
12.00-12.20Delia Kesner and Pierre Vial. Quantitative Types for the Lambda-Mu Calculus with Explicit and Implicit Replacement
12.20-12.40Gilles Dowek. Models and termination of proof reduction in the lambda Pi-calculus modulo theory
12.40-14.20lunch
14.20-14.40Session 11 (chair: Marc Bezem)Amin Timany, Matthieu Sozeau and Bart Jacobs. Cumulative inductive types in Coq
14.40-15.00Ambrus Kaposi, András Kovács, Péter Diviánszky and Balázs Kőműves. Derivation of elimination principles from a context
15.00-15.20Neil Ghani, Conor McBride, Fredrik Nordvall Forsberg and Stephan Spahn. Inductive-Recursive Definitions and Composition
15.20-15.40Paolo Capriotti. Notions of type formers
15.40-16.00Thorsten Altenkirch and Gun Pinyo. Monadic containers and universes
16.00-16.30coffee break
16.30-16.50Session 12 (chair: Nicolai Kraus)Bashar Igried and Anton Setzer. Strong Bisimilarity Implies Trace Semantics in CSP-Agda
16.50-17.10Tarmo Uustalu and Niccolò Veltri. Partiality and container monads
17.10-17.30Ian Orton and Andrew Pitts. Axioms for Univalence
17.30-17.50Robin Adams and Andrew Polonsky. A Type Theory with Native Homotopy Universes
17.50-18.10Felix Rech and Steven Schäfer. A Small Basis for Homotopy Type Theory
18.10-18.40TYPES conference business meeting
18.40-22.30conference dinner

1 June (Thursday)

9.00-10.00Session 13 (chair: Herman Geuvers)INVITED TALK: Edwin Brady. An Architecture for Dependently Typed Applications in Idris
10.00-10.20coffee break
10.20-10.40Session 14 (chair: Keiko Nakata)Rodolphe Lepigre. Theory and Demo of PML2: Proving Programs in ML
10.40-11.00Manuel Bärenz and Sebastian Seufert. Verifying Functional Reactive Programs with Side Effects
11.00-11.20Thibaut Balabonski, Marco Gaboardi, Chantal Keller and Benoît Valiron. Regularity for Free
11.20-11.40coffee break
11.40-12.00Session 15 (chair: Anders Mörtberg)Anton Setzer. Modelling Bitcoins in Agda
12.00-12.20Guillaume Brunerie. The Steenrod squares in homotopy type theory
12.20-12.40Luís Cruz-Filipe, Joao Marques-Silva and Peter Schneider-Kamp. The Boolean Pythagorean Triples Problem in Coq
12.40-14.20lunch
14.20-14.40Session 16 (chair: Andrej Bauer)Thorsten Altenkirch, Paolo Capriotti and Bernhard Reus. Domain Theory in Type Theory via QIITs
14.40-15.00Thorsten Altenkirch, Paolo Capriotti, Thierry Coquand, Nils Anders Danielsson, Simon Huber and Nicolai Kraus. Type Theory with Weak J
15.00-15.20Sergei Soloviev. On Certain Group Structures in Type Theory
15.20-15.40Colin Riba and Pierre Pradic. A Curry-Howard Approach to Church's Synthesis
15.40-16.00Georgiana Elena Lungu and Zhaohui Luo. Extensions by Definition in Type Theory
16.00-16.30coffee break
16.30-16.50Session 17 (chair: Thorsten Altenkirch)Andreas Nuyts, Andrea Vezzosi and Dominique Devriese. Parametric Quantifiers for Dependent Types
16.50-17.40DISCUSSION SESSION. On extensionality, led by Thorsten Altenkirch

Excursion (30 May)

Sightseeing tour by bus with English speaking guide. During the guided tour our guests get acquainted with the most beautiful sights of Budapest, have a short walk in Buda Castle including entrance to Matthias Church. The last stop of the program is a visit in a wine cellar (called Budafok Wine Town) in South Buda region. Wine tasting with assistance of a skilled Sommelier in the Zaborszky Cellar.

 

Departure time:15.30 h
Meeting point:at Danube gate of the Conference venue (1117 Budapest, Pázmány Péter sétány 1/c)
The excursion ends:approx. 20.00 h at the Conference venue
Price:EUR 30 / person
Please note:Minimum number of participants: 30. After 23 May, registration is subject to available places left.

Conference dinner (31 May)

Sightseeing on the Danube with dinner on Boat „Sirona”. During the 3-hour boat trip our guests can enjoy the wonderful panorama of the illuminated city, while a tasteful buffet dinner including drinks will be served on board.

 

Departure time:19.00 h
Place of the departure:ELTE Lágymányosi Dock, opposite to Conference venue (1117 Budapest, Pázmány Péter sétány 1/C)
47°28'18.8"N 19°03'52.8" (see map)
Meeting time:18.40 h
Meeting point: at Danube gate of the Conference venue (1117 Budapest, Pázmány Péter sétány 1/c)
The boat trip ends: at 22.30 at the pier at Jászai Mari tér, close to Margaret bridge on the Pest side (see map)

The Conference Dinner is included in registration fee (regular/students).

Price of the extra ticket: EUR 50 / person.

PROGRAM COMMITTEE



TRAVEL INFORMATION

The currency is Hungarian Forint (HUF), around 300 HUF is worth 1 Euro. You can use debit/credit cards in almost every shop and restaurant, but you may need cash in small pubs. The cheapest way to get cash is from an exchange bureau in the city centre. Ask your hotel or follow these instructions.

Travel to Budapest

  • By flight to Budapest Liszt Ferenc International Airport.
  • By train: 2.5 hours journey from Vienna, direct trains from Berlin, Munich, Prague, Warsaw, Zurich etc. Search trains on bahn.de, buy tickets online from the respective train companies. International tickets from the Hungarian train company have to be printed at a kiosk at a train station in Hungary.
  • By car: you can park your car next to the university for free at your own risk.

Travel from the airport to the city centre

  • BKK bus 200E takes you to the nearest metro station Kőbánya-Kispest, you can take metro line 3 from there to the city centre. The bus stop is just outside the terminal building. You can use the bus with normal BKK tickets (300 HUF), see below for information. Google maps journey planner knows about the timetable, also here is a direct link.
  • Airport minibus service, you can book it online or at the terminal in person after arrival. A minibus ride to the city centre costs around 7 times as much as public transportation and is around one third the travel time.
  • You can take a taxi from the airport, it is recommended to book a taxi at the Főtaxi kiosk just outside the terminal building. Note that COST does not normally pay for taxi expenses, see section 4.1.4, page 30 of the COST Vademecum. A taxi ride to the city centre costs around 14 times as much as public transportation and is around one third the travel time.

Travel within the city centre

  • Public transportation (BKK) is the fastest and cheapest way to get around in Budapest. You can use Google maps to plan your journey, it knows about all bus, trolley bus, tram and metro lines. It is recommended to buy a 5/30 BKK travelcard for 4550 HUF at the airport, you can use this for 5 times 24 hours during a month. Alternatively, you can buy 10 tickets for 3000 HUF: one ticket is only valid for a single bus/tram ride, if you change to another bus, you have to validate a new ticket (however you can change metro lines with a single ticket). You can buy tickets at the kiosk at the airport or from the ticket machines which accept debit/credit cards. There are machines next to the bus stop at the airport and at all metro stations, and at most tram stops. The conference venue is near the following BKK stops:
  • Public bicycle: you can use the green public bicycles in the city centre, see BUBI website for information (BUBI = Budapest Bicycle). There is a BUBI docking station next to the conference venue. A weekly pass is 2000 HUF, and you can use a bicycle for 30 minutes without paying extra. You can buy a pass at the airport BKK kiosk or BKK Customer Service Points.
  • Walking is cheap and nice.
  • Taxi. Note that COST does not normally pay for taxi expenses, see section 4.1.4, page 30 of the COST Vademecum.

VENUE

The conference will be held in the Lágymányos South Building of Eötvös Loránd University, see the map below. The address is Pázmány Péter sétány 1/C, Budapest 1117, Hungary. Look for the red hat on the following map. The lecture hall we will use is 0-823 Kitaibel Pál room, very close to the West entrance of the building which is marked with an arrow on the map.

Wifi access: you can use eduroam or the network Types2017 with password TypeTheoryApps.




ACCOMMODATION

We reserved 55 rooms altogether in the following hotels (see the above map):

  • Hotel Erzsébet City Centre (15 rooms, single room: 95 EUR/day, double room: 103 EUR/day, reservation deadline 21 April), booking form
  • Leonardo Hotel Budapest (15 rooms, single room: 85 EUR/day, double room: 95 EUR/day, reservation deadline 10 May), booking form
  • Hotel Flamenco (no rooms left), booking form
To get the above prices, please fill out the booking form and send it to the hotel through email, fax or post or just call the hotel.

Services such as booking.com and airbnb.com are known to work well in Budapest too.

The judgemental map of Budapest (google) is quite accurate about what the different areas are like. The conference venue is in the "more nerds" area.