Sciweavers

POPL
2016
ACM
8 years 8 months ago
Dependent types and multi-monadic effects in F
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Asee...
POPL
2016
ACM
8 years 8 months ago
System f-omega with equirecursive types for datatype-generic programming
Traversing an algebraic datatype by hand requires boilerplate code which duplicates the structure of the datatype. Datatype-generic programming (DGP) aims to eliminate such boiler...
Yufei Cai, Paolo G. Giarrusso, Klaus Ostermann
POPL
2016
ACM
8 years 8 months ago
Fabular: regression formulas as probabilistic programming
Regression formulas are a domain-specific language adopted by several R packages for describing an important and useful class of statistical models: hierarchical linear regressio...
Johannes Borgström, Andrew D. Gordon, Long Ou...
POPL
2016
ACM
8 years 8 months ago
Memoryful geometry of interaction II: recursion and adequacy
A general framework of Memoryful Geometry of Interaction (mGoI) is introduced recently by the authors. It provides a sound translation of lambda-terms (on the high-level) to their...
Koko Muroya, Naohiko Hoshino, Ichiro Hasuo
POPL
2016
ACM
8 years 8 months ago
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
Despite much research on concurrent programming languages, especially for Java and C/C++, we still do not have a satisfactory definition of their semantics, one that admits all c...
Jean Pichon-Pharabod, Peter Sewell
POPL
2016
ACM
8 years 8 months ago
Combining static analysis with probabilistic models to enable market-scale Android inter-component analysis
Static analysis has been successfully used in many areas, from verifying mission-critical software to malware detection. Unfortunately, static analysis often produces false positi...
Damien Octeau, Somesh Jha, Matthew Dering, Patrick...
POPL
2016
ACM
8 years 8 months ago
Taming release-acquire consistency
We introduce a strengthening of the release-acquire fragment of the C11 memory model that (i) forbids dubious behaviors that are not observed in any implementation; (ii) supports ...
Ori Lahav, Nick Giannarakis, Viktor Vafeiadis
POPL
2016
ACM
8 years 8 months ago
Modelling the ARMv8 architecture, operationally: concurrency and ISA
In this paper we develop semantics for key aspects of the ARMv8 multiprocessor architecture: the concurrency model and much of the 64-bit application-level instruction set (ISA). ...
Shaked Flur, Kathryn E. Gray, Christopher Pulte, S...
POPL
2016
ACM
8 years 8 months ago
Newtonian program analysis via tensor product
Recently, Esparza et al. generalized Newton’s method—a numerical-analysis algorithm for finding roots of real-valued functions—to a method for finding fixed-points of sys...
Thomas W. Reps, Emma Turetsky, Prathmesh Prabhu
POPL
2016
ACM
8 years 8 months ago
Learning invariants using decision trees and implication counterexamples
Inductive invariants can be robustly synthesized using a learning model where the teacher is a program verifier who instructs the learner through concrete program configurations...
Pranav Garg 0001, Daniel Neider, P. Madhusudan, Da...