Events and news relevant to the Laboratory for Foundations of Computer Science

[Ohad Kammar <ohad.kammar@ed.ac.uk>]

Hi,

We'll have an LFCS seminar next week:

  Friday, 15 Aug, 11.10am

  Note unusual day and time!

  J. Garrett Morris, The University of Iowa

  This seminar is hybrid.

  

  Venue: IF G.03

  

  To attend remotely:

  URL:  https://ed-ac-uk.zoom.us/j/89536407490

  Password: ZC2akwpN

We're synchronising the seminar time with the teaching timetable, and

plan to start the talk at the advertised time, so please arrive a minute or two

earlier.

In detail:

----------------------------------------------------------------------

J. Garrett Morris, The University of Iowa

https://jgbm.github.io/

  Friday, 15 Aug, 11.10am

  Note unusual day and time!

  Venue: IF G.03

  Remote participation:

  URL:  https://ed-ac-uk.zoom.us/j/89536407490

  Password: ZC2akwpN

Title: On Extensibility

Abstract

The _expression_ problem is an old name for an older problem: to

independently extend the definition of a data type and the operations

over it, without recompiling existing code and while retaining static

type safety. I am interested in an extension of the _expression_ problem:

to define data types and operations over them by combining independent

definitions of smaller data types, and operations over those smaller

types. As I will demonstrate, a solution to this problem provides both

flexible combination of data types and functions and precise

definitions of traversals over recursive data types.

I will present the Rose type system, the current state of a line of work

which (I claim!) solves the extended _expression_ problem. Our work is

founded on row types, which make structures of data first-class

citizens of the type system. We have a novel approach to row typing, in

which operations on rows are described by predicates in a qualified

type system. Rose supports label-generic programming, an extension

to row typing that captures generic programming patterns without

relying on run-time type representation. We have extended Rose to

recursive types, and discovered a new formulation of extensible

recursive traversals. I will shown that the resulting system is

sufficient to capture several examples of extensible programming,

including extensible big-step and small-step evaluation relations,

and modular definitions of desugaring and substitution.

Rose has a formal model with the expected metatheory, mechanized in

Agda, and an experimental implementation, sufficient to type check

and evaluate the examples in the talk.

Speaker bio:

J. Garrett Morris is an assistant professor and the inaugural

Emeriti-Faculty Scholar in the Department of Computer Science at the

University of Iowa. He received his Ph.D. from Portland State

University in Oregon, and post-doctoral training at the University of

Edinburgh, Scotland. His research focuses on the development of type

systems for higher-order functional programming languages,

particularly on problems of extensibility and modularity. His work is

supported by the National Science Foundation, including by a CAREER

award.

----------------------------------------------------------------------

Upcoming seminars:

------------------

28 Oct: Patrick Totzke, University of Liverpool: Optimally Controlling a Random

        Population

23 Sep: Paul Goldberg, University of Oxford

30 Sep: Leslie Ann Goldberg, University of Oxford

07 Oct: Zongchen Chen, Georgia Institute of Technology (Georgia Tech)

14 Oct: Bruno Cavalar, University of Oxford

21 Oct: Xinyuan Zhang, Nanjing University

If you would like to propose a speaker, or speak yourself, please contact me.

The seminar webpages:

http://web.inf.ed.ac.uk/lfcs/events/lfcs-seminars

Yours,

Ohad.

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.