Sciweavers

Share
POPL
2016
ACM
3 years 2 months ago
Pushdown control-flow analysis for free
Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollut...
Thomas Gilray, Steven Lyde, Michael D. Adams 0001,...
POPL
2016
ACM
3 years 2 months ago
Effects as sessions, sessions as effects
Effect and session type systems are two expressive behavioural type systems. The former is usually developed in the context of the λcalculus and its variants, the latter for the ...
Dominic A. Orchard, Nobuko Yoshida
POPL
2016
ACM
3 years 2 months ago
PSync: a partially synchronous language for fault-tolerant distributed algorithms
Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, d...
Cezara Dragoi, Thomas A. Henzinger, Damien Zuffere...
POPL
2016
ACM
3 years 2 months ago
Example-directed synthesis: a type-theoretic interpretation
Input-output examples have emerged as a practical and user-friendly specification mechanism for program synthesis in many environments. While example-driven tools have demonstrat...
Jonathan Frankle, Peter-Michael Osera, David Walke...
POPL
2016
ACM
3 years 2 months ago
Breaking through the normalization barrier: a self-interpreter for f-omega
According to conventional wisdom, a self-interpreter for a strongly normalizing λ-calculus is impossible. We call this the normalization barrier. The normalization barrier stems ...
Matt Brown, Jens Palsberg
POPL
2016
ACM
3 years 2 months ago
Type theory in type theory using quotient inductive types
We present an internal formalisation of dependent type theory in type theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient induct...
Thorsten Altenkirch, Ambrus Kaposi
POPL
2016
ACM
3 years 2 months ago
Binding as sets of scopes
Our new macro expander for Racket builds on a novel approach to hygiene. Instead of basing macro expansion on variable renamings that are mediated by expansion history, our new ex...
Matthew Flatt
books