Linear Haskell: Practical linearity in a higher-order polymorphic language

January 24, 2018 ~ Adrian Colyer ~ 5 Comments

Linear Haskell: Practical linearity in a higher-order polymorphic language Bernardy et al., POPL 18 I went in expecting this paper to be hard work. I mean, (a) it’s a POPL paper, (b) it’s about Haskell, and (c) not only is it about Haskell, it’s about an extension to the Haskell type system! I was more ... Continue Reading

Programming and proving with distributed protocols

January 22, 2018 ~ Adrian Colyer ~ Leave a comment

Programming and proving with distributed protocols Sergey et al., POPL 18 Last week we looked at the verification of Rust’s type-based safety guarantees, and a verification toolchain for proving properties of JavaScript programs. Today it’s the turn of Disel, a framework for developing and verifying message-passing based distributed systems (it would seem to fit beautifully ... Continue Reading

JaVerT: JavaScript Verification Toolchain

January 19, 2018 ~ Adrian Colyer ~ 4 Comments

JaVerT: JavaScript Verification Toolchain Santos et al., POPL 18 The JavaScript Verification Toolchain (JaVerT) is designed to support reasoning over JavaScript programs. It can be used to verify functional correctness properties of programs annotated with pre- and post- conditions, loop invariants, and instructions for unfolding and folding user-defined predicates. To do this, it must be ... Continue Reading

RustBelt: securing the foundations of the Rust programming language

January 18, 2018 ~ Adrian Colyer ~ 2 Comments

RustBelt: Securing the foundations of the Rust programming language Jung et al., POPL, 2018 Yesterday we saw the value of meta-engineering development processes in order to produce better (more secure) outcomes. Included in Bernstein’s recommendations was careful selection of programming language. Rust is a language in that spirit. It has long been a “holy grail” ... Continue Reading

A model for reasoning about JavaScript promises

November 10, 2017 ~ Adrian Colyer ~ 1 Comment

A model for reasoning about JavaScript promises§ Madsen et al., OOPSLA’17 As an antidote to callback-hell, ECMAScript 6 introduces Promises. Promises represent the value of an asynchronous computation, and the functions resolve and reject are used to settle the promise. Promises can be chained using then. However, the semantics of JavaScript promises are quite complex, ... Continue Reading

Type test scripts for TypeScript testing

November 9, 2017 ~ Adrian Colyer ~ 2 Comments

Type test scripts for TypeScript testing Kristensen et al., OOPLSA’17 Today’s edition of The Morning Paper comes with a free tongue-twister; ‘type test scripts for TypeScript testing!’ One of the things that people really like about TypeScript is the DefinitelyTyped repository of type declarations for common (otherwise untyped) JavaScript libraries. There are over 3000 such ... Continue Reading

Fast and precise type checking for JavaScript

November 8, 2017 ~ Adrian Colyer ~ 3 Comments

Fast and precise type checking for JavaScript Chaudhuri et al., OOPSLA’17 In this paper we present the design and implementation of Flow, a fast and precise type checker for JavaScript that is used by thousands of developers on millions of lines of code at Facebook every day. In a pretty dense 30 pages, ‘Fast and ... Continue Reading

To type or not to type: quantifying detectable bugs in JavaScript

September 19, 2017 ~ Adrian Colyer ~ 50 Comments

To type or not to type: quantifying detectable bugs in JavaScript Gao et al., ICSE 2017 This is a terrific piece of work with immediate practical applications for many project teams. Is it worth the extra effort to add static type annotations to a JavaScript project? Should I use Facebook's Flow or Microsoft's TypeScript if ... Continue Reading

Bringing the web up to speed with WebAssembly

September 18, 2017 ~ Adrian Colyer ~ 7 Comments

Bringing the web up to speed with WebAssembly Haas et al., PLDI 2017 This is a joint paper from authors at Google, Mozilla, Microsoft and Apple describing the motivations for WebAssembly together with a very concise exposition of its core semantics. If you're following along with the paper, I found it helpful to dip into ... Continue Reading

JavaScript for extending low-latency in-memory key-value stores

August 22, 2017 ~ Adrian Colyer ~ 10 Comments

JavaScript for extending low-latency in-memory key-value stores Zhang & Stutsman, HotCloud'17 Last year we looked at RAMCloud, an ultra-low latency key-value store combining DRAM and RDMA. (Also check out the team's work on patterns for writing distributed, concurrent, fault-tolerant code and how to support linearizable multi-object transactions on RAMCloud with RIFL). Now the RAMCloud research ... Continue Reading

the morning paper

a random walk through Computer Science research, by Adrian Colyer
Made delightfully fast by strattic

Programming Languages