A theory of the learnable

January 31, 2018 ~ Adrian Colyer ~ 7 Comments

A theory of the learnable Valiant, CACM 1984 (Also available in ) Today’s paper choice comes from the recommend study list of Prof. Margaret Martonosi’s 2015 Princeton course on “Great moments in computing.” A list I’m sure we’ll be dipping into again! There is a rich theory of computation when it comes to what we ... Continue Reading

The paradigms of programming

January 29, 2018 ~ Adrian Colyer ~ 18 Comments

The paradigms of programming Floyd, CACM 1979 (Also available in ) A couple of weeks ago we looked at Dan Bernstein’s very topical “thoughts on security after ten years of qmail 1.0.” From the general reaction I can tell that lots of you enjoyed reading that paper, but in the discussions that I saw, no-one ... Continue Reading

A practitioner’s guide to reading programming languages papers

January 26, 2018 ~ Adrian Colyer ~ 25 Comments

Last week I jokingly said that POPL papers must pass an ‘intellectual intimidation’ threshold in order to be accepted. That’s not true of course, but it is the case that programming languages papers can look especially intimidating to the practitioner (or indeed, the academic working in a different sub-discipline of computer science!). They are full ... Continue Reading

A static verification framework for message passing in Go using behavioural types

January 25, 2018 ~ Adrian Colyer ~ 1 Comment

A static verification framework for message passing in Go using behavioural types Lange et al., ICSE 18 With thanks to Alexis Richardson who first forwarded this paper to me. We’re jumping ahead to ICSE 18 now, and a paper that has been accepted for publication there later this year. It fits with the theme we’ve ... Continue Reading

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

Why is random testing effective for partition tolerance bugs?

January 23, 2018 ~ Adrian Colyer ~ 1 Comment

Why is random testing effective for partition tolerance bugs? Majumdar & Niksic, POPL 18 A little randomness is a powerful thing! It can make the impossible possible (FLP ), balance systems remarkably well (the power of two random choices), and of course underpin much of cryptography. Today’s paper choice examines the unreasonable effectiveness of random ... 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

Some thoughts on security after ten years of qmail 1.0

January 17, 2018 ~ Adrian Colyer ~ 21 Comments

Some thoughts on security after ten years of qmail 1.0 Bernstein, 2007 I find security much more important than speed. We need invulnerable software systems, and we need them today, even if they are ten times slower than our current systems. Tomorrow we can start working on making them faster. That was written by Daniel ... Continue Reading

the morning paper

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

Month: January 2018