Date/Time
Date(s) - 18/02/2015
All Day
Location
Royal College Building, University of Strathclyde
Wednesday 18 February, 12:00-1700
Royal College Building, room RC512, George Street, Glasgow, G1 1XW
http://www.strath.ac.uk/maps/royalcollegebuilding/
Programme:
12:00 – 13:00 lunch
13:00 – 14:00 the session session
Dominic Orchard (Imperial College): Effects in a pi
Sam Lindley (Edinburgh): A semantics for propositions as sessions
14:00 – 14:30 coffee
14:30 – 15:30 the haskelly rascals
Wim Vanderbauwhede (Glasgow): A Prototype-based Perl Type System for Interaction with Haskell
Adam Gundry Well-Typed, Strathclyde): Units of measure as a GHC plugin
15:30 – 16:00 more coffee
16:00 – 17:00 actors and algebras
Paul Harvey (Glasgow)@ An Actor-based Programming Language for the Internet of Things and Concurrency
Bob Atkey (Edinburgh, but not for much longer…): An Algebraic Approach to Typechecking and Elaboration
17:00 – 18:00 drinks (and ravening) at The Raven, 81-85 Renfield Street, Glasgow, G2 1NQ
http://www.theravenglasgow.co.uk/the-raven/about/find-us.html
18:00 – 20:00ish dinner at Yiamas, 16-20 Bath Street, Glasgow, G2 1HB
http://yiamasglasgow.webs.com/contact-us
and after that, who knows what…?
Abstracts
Dominic Orchard: Effects in a pi
Concurrent programming with state is difficult: a mutable store provides an implicit source of asynchronous interaction which is often difficult to reason about. In this talk, I propose a foundation for reasoning about concurrent state effects using session types. I show that session types are expressive enough to encode a traditional effect system for state. This is formalised via an effect-preserving embedding of an impure functional language with an effect system into the pi-calculus with session types. The usual pi-calculus encoding of mutable memory cells/operations is used, and its session typing is shown to be isomorphic to a causal state effect annotation. This provides a way to specify, reason about, and control the scope of concurrent side effects.
Sam Lindley: A semantics for propositions as sessions
Session types provide a static guarantee that concurrent programs respect communication protocols. Recently, Caires, Pfenning, and Toninho, and Wadler, have developed a correspondence between propositions of linear logic and session-typed calculus processes. We relate the cut-elimination semantics of this approach to an operational semantics for session-typed concurrency in a functional language. We begin by presenting a variant of Wadler’s session-typed core functional language, GV. We give a small-step operational semantics for GV. We develop a suitable notion of deadlock, inspired by existing accounts of deadlock in pi-calculus, and show that all well-typed GV programs are deadlock-free, deterministic, and terminating. We relate GV to linear logic by giving translations between GV and CP, a process calculus with a type system and semantics based on classical linear logic. We prove that both directions of our translation preserve reduction; previous translations from GV to CP, in contrast, fail to preserve beta-reduction. Furthermore, to demonstrate the modularity of our approach, we define two extensions of GV which preserve deadlock-freedom, determinism, and termination.
Wim Vanderbauwhede: A Prototype-based Perl Type System for Interaction with Haskell
To gradually port a large codebase from Perl to Haskell I developed a way to call Haskell functions from Perl, as transparently as possible. In general, the only way to guarantee the correctness of the types of the function arguments in Haskell is to ensure they are well-typed in Perl. So I ended up writing a Haskell-inspired type system for Perl. In this talk I will first discuss the approach I took to call Haskell from Perl, and then the reasons why a type system is needed, and the actual type system I developed. The type system is based on “prototypes”, functions that create type descriptors, and a small API of functions to create type constructors and manipulate the types. The system is type checked at run time and supports sum types, product types, function types and polymorphism. The approach is not Perl-specific and suitable for other dynamic languages.
Adam Gundry: Units of measure as a GHC plugin
Typed functional programming and units of measure are a natural combination, as F# demonstrates. However, encoding statically-checked units in Haskell’s type system leads to inevitable disappointment, and extending the language itself sounds too much like hard work! I’ll show how a tiny new feature of the upcoming GHC 7.10 will enable domain-specific constraint solving in the typechecker, making it possible to implement units of measure as a type system extension without so much as recompiling GHC.
Paul Harvey: An Actor-based Programming Language for the Internet of Things and Concurrency
Everything is connected and everything is happening in parallel! This statement is either true, or the direction that computing technology is heading in. Unfortunately, current programming practice is not well suited to this due to the presence of shared state and thread-based models which often lead to race conditions in non-trivial applications, and semantically bankrupt out-of-language apis which facilitate distributed communication. This talk will describe a new actor-based language called Ensemble. The language runs on a range of platforms including battery-powered computers, RaspberryPis, and desktops, as well as GPUS and Multicore CPUS. It natively supports location transparency via message passing, and runtime reconfiguration of actors across these platforms, including migration.
Bob Atkey: An Algebraic Approach to Typechecking and Elaboration
Since the work of Fiore, Plotkin and Turi, we have known that the syntax of typed and untyped lambda-calculi can be thought of in terms of algebraic theories. The typechecking process that takes us from untyped to typed terms is defined by structural recursion on the initial algebra of untyped terms. In this talk, I’ll explore the idea that the typechecking process *itself* can be expressed as an algebraic theory. This leads naturally to the idea of the programs that the programmer enters being “active” in the sense that they can participate in the type checking process, blending features of LCF-style tactic scripts with more normal terms.
