Bob Atkey's blog
Yesterday I had a lovely day at Fun in the REPL in Bristol. Alex Kavvos invited me to give a talk, so I decided to give an updated and extended version of the Data types with Negation talk I gave a few times last year. I've got a bit further in working out how to analyse the semantics of a data type with negation, but seeing an analogy with the solutions of mixed-variance domain equations. Here…
I just gave a talk at Certified Programs and Proofs on our paper Compiling higher-order specifications to SMT solvers . Slides: It is a description of the type based analysis approach that we use in the Vehicle specification language to discover when the queries that a user writes are actually translatable to an SMT solver. Based on this type based analysis we either give the user a nice error…
Catala is a programming language for the law. As described in an ICFP 2021 paper by Merigoux et al. , Catala has multiple features designed for making it easy to write code that implements legal texts. The feature I want to talk about here is Catala's support for default reasoning. Default reasoning involves rules like “X is the case, except when Y, Z, ...”. Apparently, such patterns are common in…
Back in April and June last year, at MSFP and at TYPES, I gave talks about some work I've done on trying to understand what it would mean to allow negation in data type definitions. The gist of the talk is: what if we could define a predicate for even numbers like this in Agda (or Coq or Idris or Lean): data Even : Nat → Set where zero : Even 0 suc : ∀ {n} → not (Even n) → Even (suc n) So 0 is…
Last Friday, I gave a talk (virtually) at the CCS Colloquim at Augusta University, hosted by Harley Eades III . The title was “Resource Constrained Programming with Full Dependent Types” and the abstract was: I will talk about a system that combines Dependent Types and Linear Types. As an application of this system, I will show how to transport Martin Hofmann’s LFPL and Amortised Resource analysis…
This post contains a development of an Agda proof that, for the Call-by-Name (CBN) λ-calculus, the number of steps needed to reduce a term to weak head normal form (WHNF) in the Krivine Abstract Machine (KAM) is equal to the size of the term's typing derivation in a non-idempotent intersection type system. The inverse also holds: if a term reduces to WHNF in the KAM, then it has a typing…
Yesterday, I gave a talk entitled “Resource Constrained Programming with Full Dependent Types” at the IRIF Proofs, Programs and systems seminar in Paris. Many thanks to Paul-André Melliès for inviting me to give a talk. Abstract: I will talk about a system that combines Dependent Types and Linear Types. As an application of this system, I will show how to transport Martin Hofmann's LFPL and…
This year I am the programme chair for Off the Beaten Track 2017 ! This will be held on 21st January 2017, co-located with POPL 2017 in Paris, France. Background Programming language researchers have the principles, tools, algorithms and abstractions to solve all kinds of problems, in all areas of computer science. However, identifying and evaluating new problems, particularly those that lie…
Let's assume that you're querying to some database stored in the cloud (i.e., on someone else’s computer). Being of a sceptical mind, you worry whether or not the answers you get back are from the database you expect. Or is the cloud lying to you? Authenticated Data Structures (ADSs) are a proposed solution to this problem. When the server sends back its answers, it also sends back a “proof” that…
Here are the slides I used for my keynote talk for the afternoon at this year’s Off the Beaten Track workshop in St. Petersburg, Florida, USA. Many thanks to Lindsey Kuper for inviting me to give a talk and for organising it all. The talk wasn’t recorded, but here is a collection of notes to go with the things I talked about: The Abstract is ‘an Enemy’ is a paper by Alan F. Blackwell, Luke Church,…
Back in February, the paper A theory of changes for higher-order languages — incrementalizing λ-calculi by static differentiation by Cai, Giarusso, Rendel, and Ostermann, was posted to Lambda-the-Ultimate . The poster, gasche, made the following parenthetical comment at the end of the L-t-U post: (The program transformation seems related to the program-level parametricity transformation.…
Two months at the Scottish Programming Languages Seminar , February 2015 Strathclyde Edition, I gave a talk entitled “ An Algebraic Approach to Typechecking and Elaboration ”. Several people have asked me to put the slides online, so here they are: The point of the talk was to present an algebraic approach to specifying type systems ─ algebraic in the sense of algebraic theories with operations…
The make program is a widely used tool for building files from existing files, according to a set of build rules specified by the user. It is usually used to compile executable programs from source code, but can also be used for many other jobs where a bunch of things are generated from other things, like this website, for example. Many alternatives to make have been proposed. Motivations for…
I gave two talks at POPL 2014 , back to back. This was pretty frightening beforehand, but seemed to go alright. Here are the slides: From Parametricity to Conservation Laws, via Noether's Theorem A Relationally Parametric Model of Dependent Type Theory
One paper finished, two new ones submitted. Productive Coprogramming Conor and I have just submitted the final version of "Productive Coprogramming with Guarded Recursion" to the publishers. Looking forward to ICFP in Boston! Pair of Papers Pertaining to Parametricity Dependent Types With Neil and Patty , we've constructed a relationally parametric model of impredicative and predicative dependent…
Conor McBride and I have just submitted a new paper to ICFP. In it, we attempt to use Nakano-style guarded recursion to write productive coprograms. This is an elaboration of Conor's blog post and the slides I posted here a while ago. Here's a link to the paper, and the abstract: Total functional programming offers the beguiling vision that, just by virtue of the compiler accepting a program, we…
Patricia Johann , Andrew Kennedy and I have a new paper that will be presented at POPL in January! This paper is an extension of Andrew's POPL'97 paper on interpreting dimension types in terms of scaling invariance. Here's a link to the paper and the abstract: Reynolds' relational parametricity provides a powerful way to reason about programs in terms of invariance under changes of data…
I gave a talk last night at the Ed Lambda , the Edinburgh functional programming meetup, on “Theorems for Free”. This was (I hope) a fairly high-level talk about how free theorems are derived, and some extensions to other kinds of polymorphism that I've worked on recently. Here are the slides I used: I didn't include much in the way of references to the literature in the talk, but the main paper…
Patricia Johann, Neil Ghani, Bart Jacobs and myself have just submitted a paper on interleaving pure data types with effects. This is a much more detailed version of the blog post I wrote back in January on reasoning about stream processing with effects. Here is the abstract: The study of programming with and reasoning about inductive datatypes such as lists and trees has benefited from the simple…
I just gave a talk at CSL 2012 on "Relational Parametricity for Higher Kinds". In the paper I explain how to extend the usual relationally parametric models of polymorphic types to handle higher kinded types, like the ones found in Haskell and Scala. As a consequence, you get encodings of things like equality types, higher-kinded existential types and higher-kinded initial algebras, with nice…
It is a truth, universally acknowledged, that any programming technique must be in want of a reasoning principle. Stream processing in Haskell is very much in the air at the moment, what with Iteratees (as embodied in the Enumerator library), Conduits and probably some more that I don't know about. Patty Johann , Neil Ghani , Bart Jacobs and I have recently had the paper "Fibrational Induction…
I've been hacking a bit on Foveran lately. The main new thing that I've added is the integration of the monad laws and functor laws into the definitional equality. These additions were inspired by some suggestions of Conor, and a post on Epilogue by Pierre from some time back. I've taken a different implementation approach to the one sketched in that blog post. The scheme I am using is Filinski's…
On Friday, I gave a talk at the Scottish Programming Languages Seminar (SPLS) at Heriot-Watt . Many thanks to Greg Michaelson for organising everything and giving me time to speak. I've put the slides I used on-line as a PDF file (with two small fixes, see below). The talk presents an extension of a Nakano-style typed λ-calculus with a delay modality for guarded recursion. In short, this means:…
Last time I talked about the background on defining structurally recursive functions in Type Theory and why you might want it. The key point is that structural recursion is driven by the data that is being analysed, as opposed to just doing its own thing with a side-proof that it always terminates. The goal here is to come up with a self-contained and syntax-free definition of a dependently-typed…
This is the first in (hopefully) a series of blog posts on defining an algebra of structural induction principles in type theory, borrowing inspiration from category theory. This is joint work with Patty Johann and Neil Ghani , and builds on work and ideas of many, notably Conor McBride . In this post, I'll just explain the background. Structural Recursion Structural recursion is a fundamental…