This is a EUTypes WG meeting in colocation with the final meeting of BETTY, taking place 6-7 October. We will overlap on 6 October.
The meeting will take place in Caparica, in the campus of the Faculty of Science and Technology of the New University of Lisbon. For venue information and the BETTY meeting programme, see the BETTY meeting page.
On 5 Oct, we will be in the seminar room of the Informatics Department (building colored brown and labelled "CITI/CENTRIA" on the map on the BETTY page). On 6 (and 7) Oct, the meeting will be in the seminar room of the Library (building colored yellow and labelled "Bibliot.", on the ground floor).
The local organizers at UNL charge 20 EUR per day for lunches and coffee breaks and a further 20 EUR for the organized dinner on 6 Oct (which you can cover with your meals allowance from COST). You will receive a link to the local registration form by email.
For information on the EUTypes meeting, contact Tarmo Uustalu.
Danel Ahman
Luís Caires
João Costa Seco
Ugo de'Liguoro
Herman Geuvers
Silvia Ghilezan
Marco Giunti
Zhaohui Luo
Simão Melo de Sousa
Marino Miculan
Garrett Morris
Pierre-Yves Schobbens
Carsten Schürmann
Anton Setzer
Tarmo Uustalu
Danel Ahman: Recall for free: preorder-preserving state monads in F*
Slides (pdf)
Abstract: In this work, we set out to establish the formal foundations of the phenomenon that, if
then we should be able to recall for free that P also holds for any state s that s can evolve to. Many F* programs rely implicitly and pervasively on this invariant, including miTLS, an ongoing effort to verify the TLS protocol in F*.
This is joint work with Nikhil Swamy and Aseem Rastogi.
Luís Caires: Linear logic and behavioural process types
Slides (pdf)
Abstract: While type systems for more traditional programming abstractions have been rooted on pure logical principles, in the sense of Curry-Howard correspondences, the connections between session-based concurrent programming languages and their logically motivated type disciplines only started to be better understood recently. In this talk, we review recent work on the theme, in a tutorial style.
Zhaohui Luo: Linear dependent types
Slides (pdf)
Abstract: Introducing linear types (and, in general, resource sensitive types) into a type theory with dependent types has been an interesting but difficult topic. One of the most difficult issues is whether to allow types to depend on linear variables. For instance, for f : A -o A, the equality type Eq(f x, x) depends on the linear variable x of type A. In most of the existing research so far, such a dependency is not allowed: types are only allowed to depend on intuitionistic variables, but not on linear variables. In this talk, I present a dependent type theory where types may depend on linear variables and discuss related issues and applications.
Garrett Morris: The best of both worlds: linear functional programming without compromise
Slides (pdf)
Abstract: We present a linear functional calculus with both the safety guarantees expressible with linear types and the rich language of combinators and composition provided by functional programming. Unlike previous combinations of linear typing and functional programming, we compromise neither the linear side (for example, our linear values are first-class citizens of the language) nor the functional side (for example, we do not require duplicate definitions of compositions for linear and unrestricted functions). To do so, we must generalize abstraction and application to encompass both linear and unrestricted functions. We capture the typing of the generalized constructs with a novel use of qualified types. Our system maintains the metatheoretic properties of the theory of qualified types, including principal types and decidable type inference. Finally, we give a formal basis for our claims of expressiveness, by showing that evaluation respects linearity, and that our language is a conservative extension of existing functional calculi.
Carsten Schürmann: From behavioral types to logical frameworks
Slides (pdf)
Abstract: In this tutorial, I explore how the recent advances in understanding behavioral and session types affect the design and the application of type theories and next generation logical frameworks.
Anton Setzer: GUIs, object-based programming and processes in Agda
Slides (pdf)
Abstract: We introduce the notion of an object (as in object-based programming) in dependent type theory and show how to implement it in Agda. This includes two kinds of objects: objects which directly return the result and objects which have carry out some interaction with the real world before returning a result. We introduce as well state-dependent objects, a notion which naturally occurs when programming with objects in dependent type theory. We show how this can be used to develop GUIs. As it is usually done in object-oriented languages, event handlers will be given as methods of an object which will be executed when the event occurs.
Finally, we present some work on how to represent processes in dependent type theory. We consider the process algebra CSP, although most of the ideas should translate to similar process algebras as well. We represent processes in monadic form and as a coalgebra based on an atomic one step rule.
This is joint work with Andreas Abel, Stephan Adelsberger and Bashar Igried.
Tarmo Uustalu: Interaction morphisms
Slides (pdf)
Abstract: I will discuss interaction morphisms as a means to specify how a computation is to be run, provided a state in a context. An interaction morphism of a monad T and a comonad D is a family of maps TX x DY -> X x Y natural in X and Y and subject to some equations. Interaction morphisms turn out to be a natural concept with a number of neat properties. In particular, they are in a bijective correspondence with carrier-preserving functors between the categories of coalgebras of D and stateful runners of T (monad morphisms from T to state monads), but considerably more can be said.
This is joint work with Shin-ya Katsumata.
Herman Geuvers: Formal verification of C code at Radboud University Nijmegen, an overview
Slides (pdf)
Wednesday, 5 October (officially EUTypes only, but the meeting is open; seminar room of the Informatics Department)
9-10.30 Luís Caires: Linear logic and behavioural process types
10.30-11 break
11-11.45 Garrett Morris: The best of both worlds: linear functional programming without compromise
11.45-12.30 Danel Ahman: Recall for free: preorder-preserving state monads in F*
12.30-14 lunch
14-14.45 Carsten Schürmann: From behavioral types to logical frameworks
14.45-15.30 Anton Setzer: GUIs, object-based programming and processes in Agda
15.30-16 break
16-17.30 discussion
19.30 informal dinner at Topo Chiado (Rua do Carmo, 81, Lisbon)
Thursday, 6 October (overlapping with BETTY, see the programme of the BETTY meeting; seminar room of the Library)
9-10 Nobuko Yoshida: Session types and their open problems
10-10.20 Bernardo Toninho: On the logical interpretation of sessions
10.20-10.40 Luis Caires: Session types, control effects, and linear logic
10.40-11 Marco Carbone: A logical explanation of multiparty session types
11-11.30 break
11.30-12.10 Herman Geuvers: Formal verification of C code at Radboud University Nijmegen, an overview
12.10-12.30 Zhaohui Luo: Linear dependent types
12.30-12.50 Tarmo Uustalu: Interaction morphisms
12.50-14 lunch
14-15.20 BETTY talks
15.20-16 break
16-17.20 BETTY talks
19.30 organized dinner at Atira-te ao rio (Cais do Gingal, 69/70, Almada)
