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

- we can ensure that the state of a program evolves according to a preorder R,
- we have a predicate P that is stable under R, and
- we witness that P holds of some intermediate states of the program,

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)