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 Linear Haskell: Practical linearity in a higher-order polymorphic language
Tag: Programming Languages
Programming and proving with distributed protocols
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 Programming and proving with distributed protocols
JaVerT: JavaScript Verification Toolchain
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 JaVerT: JavaScript Verification Toolchain
RustBelt: securing the foundations of the Rust programming language
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 RustBelt: securing the foundations of the Rust programming language
A model for reasoning about JavaScript promises
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 A model for reasoning about JavaScript promises
Type test scripts for TypeScript testing
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 Type test scripts for TypeScript testing
Fast and precise type checking for JavaScript
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 Fast and precise type checking for JavaScript
To type or not to type: quantifying detectable bugs in JavaScript
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 To type or not to type: quantifying detectable bugs in JavaScript
Bringing the web up to speed with WebAssembly
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 Bringing the web up to speed with WebAssembly
JavaScript for extending low-latency in-memory key-value stores
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 JavaScript for extending low-latency in-memory key-value stores
the morning paper 