title: Data Refinement Refined

authors:
Jifeng He
C. A. R. Hoare
Jeff W. Sanders


venue: esop

title: Parallelization by Semantic Detection of Reductions


title: Rewriting with a Nondeterministic Choice Operator: From Algebra to Proofs


title: Lifetime Analysis for Procedure Parameters

authors:
Uwe Kastens
Michael Schmidt


title: Denotational Semantics of Nets with Nondeterminism


title: Programs as Collections of Communicating Prolog Units

authors:
Paola Mello
Antonio Natali


title: An Experiment in Practical Semantics


title: Correctness of Code Generation from a Two-Level Meta-Language


title: Pragmatic Aspects of Two-Level Denotational Meta-Languages

authors:
Hanne Riis Nielson
Flemming Nielson


title: Specification of a Tool for Viewing Program Text


title: An And-Parallel Execution Model of Logic Programs

authors:
Bernd Schwinn
Gerhard Barth


title: An Application of Abstract Interpretation of Logic Programs: Occur Check Reduction


title: Proving Entailment Between Conceptual State Specifications


title: Compiling Extended Concurrent Prolog - Single Queue Compilation

authors:
Jiro Tanaka
Makoto Kishishita


title: Automatic Parallelization of Fortran Programs in the Presence of Procedure Calls

authors:
Rémi Triolet
Paul Feautrier
François Irigoin


title: Perfect Pipelining: A New Loop Parallelization Technique

authors:
Alexander Aiken
Alexandru Nicolau


title: The PSG System: From Formal Language Definitions to Interactive Programming Environments

authors:
Rolf Bahlke
Gregor Snelting


title: LPG: A Generic, Logic and Functional Programming Language

authors:
Didier Bert
Pascal Drabik
Rachid Echahed
Olivier Declerfayt
Brigitte Demeuse
Pierre-Yves Schobbens
François Wautier


title: CEC: A System for the Completion of Conditional Equational Specifications

authors:
Hubert Bertling
Harald Ganzinger
Renate Schäfers


title: An Exception Handling Construct for Functional Languages

authors:
Manfred Bretz
Jürgen Ebert


title: New Insights into Partial Evaluation: the SCHISM Experiment


title: Implementation of Modular Algebraic Specifications


title: A Polymorphic Type System with Subtypes for Prolog

authors:
Roland Dietrich
Frank Hagl


title: Type Inference with Subtypes

authors:
You-Chin Fuh
Prateek Mishra


title: A Theory of Software Reusability

authors:
Marie-Claude Gaudel
Th. Moineau


title: Code Selection Techniques: Pattern Matching, Tree Parsing, and Inversion of Derivors

authors:
Robert Giegerich
Karl Schmal


title: A Semantics Driven Temporal Verification System

authors:
Graham Gough
Howard Barringer


title: A Functional Language for the Specification of Complex Tree Transformations


title: A Functional Language for the Specification of Complex Tree Transformations (System Exhibition)


title: Adding Relational Query Facilities to Software Development Environments


title: Compilation of Logic Programs for Restricted And-Parallelism

authors:
Dean Jacobs
Anno Langen


title: Parametric Overloading in Polymorphic Programming Languages


title: Garp: Graph Abstractions for Concurrent Programming

authors:
Simon M. Kaplan
Gail E. Kaiser


title: Algebraic Formalisation of Program Development by Transformation


title: Implementation of Lazy Pattern Matching Algorithms


title: Extending Functional Programming Towards Relations


title: Enhancing Prolog to Support Prolog Programming Environments

authors:
Alberto Martelli
Gianfranco Rossi


title: 2-level lambda-lifting

authors:
Flemming Nielson
Hanne Riis Nielson


title: Programming with Proofs: A Second Order Type Theory


title: Semantics-Based Program Integration

authors:
Thomas W. Reps
Susan Horwitz


title: QPC: QJ-based Proof Compiler - Simple Examples and Analysis


title: Deforestation: Transforming Programs to Eliminate Trees


title: On Implementing Logic Programming Languages on a Dataflow Architecture

authors:
Patrick Weemeeuw
Maurice Bruynooghe
Marleen De Haondt


title: Types in Lambda Calculi and Programming Languages

authors:
Henk Barendregt
Kees Hemerik


title: Implementation of an Interpreter for a Parallel Language in Centaur


title: Automatic Autoprojection of Higher Order Recursive Equations


title: From Interpreting to Compiling Binding Times

authors:
Charles Consel
Olivier Danvy


title: Type Inference for Action Semantics

authors:
Susan Even
David A. Schmidt

abstract: In a series of papers [11,12,13,14,15,25,26], Mosses and Watt defme action semantics, a metalanguage for high level, domain-independent formulation of denotational semantics definitions. Action semantics was designed to support readability, abstraction, modularity, and modifiability of language definitions [13,15]. In our recent work [5], we studied a combinator-based version of action semantics. We developed a typing system for actions based on types and k/nds. The types within a kind are partially ordered to reflect subtyping. We then defined a category-sorted algebra model [18,20] for the system where actions are natural transformations over interpretation functors (which map the type names and their ordering to predomains and coercion functions). Thus, an action is a family of continuous functions that behave consistently with respect to the subtyping relation. Coercion functions-even nonembeddings-disappear. The typing system and its interpretation support an ML-style type inference algorithm for action expressions. Type inference must respect the subtyping laws, so we encounter the problems discovered by Mitchell [10], Fuh and Mishra [6], and Wand [24] regarding constraints sets. But action notation and its model are formulated so that the major problems regarding constraints are "restricted away." In particular, the monotonic behavior of actions with respect to the subtyping ordering keeps the cardinality of constraints sets small and makes constraints on record types unnecessary, even in the presence of record union and concatenation operations. This paper presents our variant of action semantics and its typing system. We give the type inference algorithms, state properties that action semantics expressions satisfy, give soundness and completeness properties and explain why they hold for type inference on action semantics expressions. We also present a small example.


title: On the Expressive Power of Programming Languages


title: Higher Order Escape Analysis: Optimizing Stack Allocation in Functional Program Implementations

authors:
Benjamin Goldberg
Young Gil Park


title: Development of Concurrent Systems by Incremental Transformations


title: Set Domains


title: Resolution and Type Theory


title: A Syntactic Theory of Transparent Parameterization

authors:
Stanley Jefferson
Shinn-Der Lee
Daniel P. Friedman


title: A Backwards Analysis for Compile-time Garbage Collection

authors:
Thomas P. Jensen
Torben Æ. Mogensen


title: Techniques for Improving Grammar Flow Analysis

authors:
Martin Jourdan
Didier Parigot


title: The Specificity Rule for Lazy Pattern-Matching in Ambiguous Term Rewrite Systems


title: Graph-based Implementation of a Functional Logic Langugage

authors:
Herbert Kuchen
Rita Loogen
Juan José Moreno-Navarro
Mario Rodríguez-Artalejo


title: Eureka Definitions for Free! or Disagreement Points for Fold/Unford Transformations

authors:
Hanne Riis Nielson
Flemming Nielson


title: Symbolic Finite Differencing - Part I


title: Synthesis of Eureka Predicates for Developing Logic Programs

authors:
Maurizio Proietti
Alberto Pettorossi


title: Algebraic Properties of Program Integration


title: Arity Raiser and its Use in Program Specialization


title: Complexity Analysis for a Lazy Higher-Order Language


title: On the Weak Adequacy of Branching-Time Remporal Logic

authors:
Philippe Schnoebelen
Sophie Pinchinat


title: Implementing Finite-domain Constraint Logic Programming on Top of a Prolog-System with Delay-mechanism

authors:
Danny De Schreye
Dirk Pollet
Johan Ronsyn
Maurice Bruynooghe


title: The Value Flow Graph: A Program Representation for Optimal Program Transformations

authors:
Bernhard Steffen
Jens Knoop
Oliver Rüthing


title: Type Inference and Implicit Scaling


title: Towards the Theory of Programming in Constructive Logic


title: Model Checking and Boolean Graphs


title: SIGNAL as a Model for Real-Time and Hybrid Systems

authors:
Albert Benveniste
Michel Le Borgne
Paul Le Guernic

abstract: Hybrid Systems axe models of systems operating in real-time and handling events as well as “continuous” computations. The Signal formalism for Hybrid Systems is presented in this extended abstract. Its expressive power is discussed, and a general method to associate various formal systems with it is presented and illustrated on deriving the present Signal compiler.


title: Towards an Adequate Notion of Observation

authors:
Gilles Bernot
Michel Bidoit
Teodor Knapik


title: Proving Safety of Speculative Load Instructions at Compile Time

authors:
David Bernstein
Michael Rodeh
Shmuel Sagiv


title: Typed Norms

authors:
Annalisa Bossi
Nicoletta Cocco
Massimo Fabris


title: Compositional Refinements in Multiple Blackboard Systems

authors:
X. J. Chen
Carlo Montangero


title: Fully Persistent Arrays for Efficient Incremental Updates and Voluminous Reads


title: Back to Direct Style


title: Extraction of Strong Typing Laws from Action Semantics Definitions

authors:
Kyung-Goo Doh
David A. Schmidt


title: Detecting Determinate Computations by Bottom-up Abstract Interpretation

authors:
Roberto Giacobazzi
Laura Ricci


title: ELIOS-OBJ Theorem Proving in a Specification Language


title: Incremental Garbage Collection Without Tags


title: Approximate Fixed Points in Abstract Interpretation

authors:
Chris Hankin
Sebastian Hunt


title: Dynamic Typing


title: Automatic Parallelization of Lazy Functional Programs

authors:
Guido Hogen
Andrea Kindler
Rita Loogen


title: Reversing Abstract Interpretations

authors:
John Hughes
John Launchbury


title: A Theory of Qualified Types


title: A Semantics for Multiprocessor Systems


title: Interprocedural Type Propagation for Object-Oriented Languages


title: Using the Centaur System to for Data-Parallel SIMD Programming: A Case Study


title: The Tensor Product in Wadler's Analysis of Lists

authors:
Flemming Nielson
Hanne Riis Nielson


title: Basic Superposition is Complete

authors:
Robert Nieuwenhuis
Albert Rubio

abstract: We define equality constrained equations and clauses and use them to prove the completeness of what we have called basic superposition: a restricted form of superposition in which only the subterms not created in previous inferences is superposed upon. We first apply our results to the equational case and define an unfailing Knuth-Bendix completion procedure that uses basic superposition as inference rule. Second, we extend the techniques to completion of full first-order clauses with equality. Moreover, we prove the refutational completeness of a new simple inference system.


title: Type Inference for Partial Types is Decidable

authors:
Patrick O'Keefe
Mitchell Wand


title: Observers for Linear Types


title: A Provably Correct Compiler Generator

abstract: We have designed, implemented, and proved the correctness of a compiler generator that accepts action semantic descriptions of imperative programming languages. The generated compilers emit absolute code for an abstract RISC machine language that currently is assembled into code for the SPARC and the HP Precision Architecture. Our machine language needs no run-time type-checking and is thus more realistic than those considered in previous compiler proofs. We use solely algebraic specifications; proofs are given in the initial model.


title: An Adequate Operational Semantics for Sharing in Lazy Evaluation

authors:
S. Purushothaman
Jill Seaman


title: Modules for an Model-Oriented Specification Language: A Proposal for MetaSoft


title: Typing References by Effect Inference


title: A Theory of Primitive Objects - Scond-Order Systems

authors:
Martín Abadi
Luca Cardelli


title: Local Type Reconstruction by Means of Symbolic Fixed Point Iteration


title: An Asynchronous Algebra with Multiple Clocks

authors:
Henrik Reif Andersen
Michael Mendler


title: Foundational Issues in Implementing Constraint Logic Programming Systems


title: Programming with Behaviors in an ML Framework - The Syntax and Semantics of LCS

authors:
Bernard Berthomieu
Thierry Le Sergent


title: Characterizing Behavioural Semantics and Abstractor Semantics

authors:
Michel Bidoit
Rolf Hennicker
Martin Wirsing


title: Extending Pruning Techniques to Polymorphic Second order Lambda-Calculus


title: Lambda-Definition of Function(al)s by Normal Forms

authors:
Corrado Böhm
Adolfo Piperno
Stefano Guerrini


title: Simulation of SOS Definitions with Term Rewriting Systems


title: Strategies in Modular System Design by Interface Rewriting

authors:
Serafino Cicerone
Francesco Parisi-Presicce


title: Symbolic Model Checking and Constraint Logic Programming: a Cross-Fertilization

authors:
Marc-Michel Corsini
Antoine Rauzy


title: Compilation of Head and Strong Reduction


title: Suffix Trees in the Functional Programming Paradigm

authors:
Robert Giegerich
Stefan Kurtz


title: Type Classes in Haskell

authors:
Cordelia V. Hall
Kevin Hammond
Simon L. Peyton Jones
Philip Wadler


title: Lazy Type Inference for the Strictness Analysis of Lists

authors:
Chris Hankin
Daniel Le Métayer


title: Lazy Unification with Simplification


title: Polymorphic Binding-Time Analysis

authors:
Fritz Henglein
Christian Mossin


title: Shapely Types and Shape Polymorphism

authors:
C. Barry Jay
J. Robin B. Cockett


title: Bottom-up Grammar Analysis - A Functional Formulation

authors:
Johan Jeuring
S. Doaitse Swierstra


title: First-Class Polymorphism for ML


title: Dimension Types


title: A Synergistic Analysis for Sharing and Groundness with Traces Linearity


title: A pi-Calculus Specification of Prolog


title: A Logical Framework for Evolution of Specifications


title: A Semantics for Higher-Order Functors

authors:
David B. MacQueen
Mads Tofte


title: Pi-Nets: A Graphical Form of pi-Calculus


title: The PCKS-Machine: An Abstract Machine for Sound Evaluation of Parallel Functional Programs with First-Class Continuations

abstract: The PCKS-machine is an abstract machine that evaluates parallel functional programs with first-class continuations. Parallelism is introduced by the construct pcall, which provides a fork-and-join type of parallelism. To the best of our knowledge, the PCKS-machine is the first implementation of such a language that is proved to have a transparent construct for parallelism: every program using such a construct returns the same result as in the absence of this construct. This machine is also characterised by the non-speculative invocation of continuations whose interest is illustrated in an application. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: A Tiny Constrain Functional Logic Language and Its Continuation Semantics

authors:
Andy Mück
Thomas Streicher


title: Fully Abstract Translations and Parametric Polymorphism

authors:
Peter W. O'Hearn
Jon G. Riecke


title: A Logical Denotational Semantics for Constraint Logic Programming

authors:
Alessandra Di Pierro
Catuscia Palamidessi


title: Broadcasting with Priority


title: Towards Unifying Partial Evaluation, Deforestation, Supercompilation, and GPC

authors:
Morten Heine Sørensen
Robert Glück
Neil D. Jones


title: Algebraic Proofs of Properties of Objects


title: Narrowing-Driven Partial Evaluation of Functional Logic Programs

authors:
María Alpuente
Moreno Falaschi
Germán Vidal


title: Rewrite Systems with Abstraction and beta-Rule: Types, Approximants and Normalization

authors:
Steffen van Bakel
Franco Barbanera
Maribel Fernández


title: A Multiple-Valued Logical Semantics for Prolog

authors:
Roberto Barbuti
Paolo Mancarella


title: Removing Value Encoding Using Alternative Values in Partial Evaluation of Strongly-Typed Languages


title: A Complete Transformational Toolkit for Compilers

authors:
Jan A. Bergstra
T. B. Dinesh
John Field
Jan Heering


title: Global Analysis of Standard Prolog Programs

authors:
Francisco Bueno
Daniel Cabeza Gras
Manuel V. Hermenegildo
Germán Puebla


title: Static Detection of Pointer Errors: An Axiomatisation and a Checking Algorithm

authors:
Pascal Fradet
Ronan Caugne
Daniel Le Métayer


title: Compositional Optimization of Disjunctive Abstract Interpretations

authors:
Roberto Giacobazzi
Francesco Ranzato


title: A Rewriting Logic for Declarative Programming

authors:
Juan Carlos González Moreno
Maria Teresa Hortalá-González
Francisco Javier López-Fraguas
Mario Rodríguez-Artalejo


title: Durations for Truly-Concurrent Transitions


title: Flow Analysis in the Geometry of Interaction

authors:
Thomas P. Jensen
Ian Mackie


title: Some Practical Problems and Their Influence on Semantics


title: Compiling Haskell by Program Transformation: A Report from the Trenches


title: Parametricity and Unboxing with Unpointed Types

authors:
John Launchbury
Ross Paterson


title: Modular Denotational Semantics for Compiler Construction

authors:
Sheng Liang
Paul Hudak


title: Compositional Semantics of Non-Deterministic Synchronous Languages

authors:
Florence Maraninchi
Nicolas Halbwachs


title: Checking System Properties via Integer Programming

authors:
Stephan Melzer
Javier Esparza


title: Efficient Minimization up to Location Equivalence

authors:
Ugo Montanari
Marco Pistore
Daniel Yankelevich


title: A New Approach to Compiling Adaptive Programs

authors:
Jens Palsberg
Boaz Patt-Shamir
Karl J. Lieberherr


title: Mode and Termination Checking for Higher-Order Logic Programs

authors:
Ekkehard Rohwedder
Frank Pfenning


title: Linear Time Hierarchies for a Functional Language Machine Model


title: Integer Constraints to Stop Deforestation


title: Towards an ML-Style Polymorphic Type System for C

authors:
Geoffrey Smith
Dennis M. Volpano


title: Assumption/Commitment Rules for Dataflow Networks - With an Emphasis on Completeness


title: Towards an Expressive Language for PDE Solvers

authors:
Michael Thuné
Krister Åhlander


title: A Bisimulation Method for Cryptographic Protocols

authors:
Martín Abadi
Andrew D. Gordon


title: A Polyvariant Binding-Time Analysis for Off-line Partial Deduction

authors:
Maurice Bruynooghe
Michael Leuschel
Konstantinos Sagonas

abstract: We study the notion of binding-time analysis for logic programs. We formalise the unfolding aspect of an on-line partial deduction system as a Prolog program. Using abstract interpretation, we collect information about the run-time behaviour of the program. We use this information to make the control decisions about the unfolding at analysis time and to turn the on-line system into an off-line system. We report on some initial experiments.


title: Verifiable and Executable Logic Specifications of Concurrent Objects in Lpi

authors:
Luís Caires
Luís Monteiro


title: Complexity of Concrete Type-Inference in the Presence of Exceptions

authors:
Ramkrishna Chatterjee
Barbara G. Ryder
William Landi


title: Synchronisation Analysis to Stop Tulping

authors:
Wei-Ngan Chin
Siau-Cheng Khoo
Tat-Wee Lee


title: Propagating Differences: An Efficient New Fixpoint Algorithm for Distributive Constraint Systems

authors:
Christian Fecht
Helmut Seidl


title: Reasonong about Classess in Object-Oriented Languages: Logical Models and Tools

authors:
Ulrich Hensel
Marieke Huisman
Bart Jacobs
Hendrik Tews


title: Language Primitives and Type Discipline for Structured Communication-Based Programming

authors:
Kohei Honda
Vasco Thudichum Vasconcelos
Makoto Kubo


title: The Functional Imperative: Shape!

authors:
C. Barry Jay
Paul Steckler


title: Code Motion and Code Placement: Just Synonyms?

authors:
Jens Knoop
Oliver Rüthing
Bernhard Steffen


title: Recursive Object Types in a Logic of Object-Oriented Programs


title: Mode-Automata: About Modes and States for Reactive Systems

authors:
Florence Maraninchi
Yann Rémond


title: From Classes to Objects via Subtyping


title: Building a Bridge between Pointer Aliases and Program Dependences

authors:
John L. Ross
Shmuel Sagiv


title: A Complete Declarative Debugger of Missing Answers


title: Systematic Change of Data Representation: Program Manipulations and a Case Study


title: Concurrent Constraint Programming Based on Functional Programming (Extended Abstract)


title: A Generic Framework for Specialization (Abridged Version)


title: Constructor Subtyping

authors:
Gilles Barthe
Maria João Frade


title: A Decidable Logic for Describing Linked Data Structures

authors:
Michael Benedikt
Thomas W. Reps
Shmuel Sagiv


title: An Operational Investigation of the CPS Hierarchy

authors:
Olivier Danvy
Zhe Yang

abstract:
We explore the hierarchy of control induced by successive transformations into continuation-passing style (CPS) in the presence of "control delimiters" and "composable continuations". Specifically, we investigate the structural operational semantics associated with the CPS hierarchy.

To this end, we characterize an operational notion of continuation semantics. We relate it to the traditional CPS transformation and we use it to account for the control operator shift and the control delimiter reset operationally. We then transcribe the resulting continuation semantics in ML, thus obtaining a native and modular implementation of the entire hierarchy. We illustrate it with several examples, the most significant of which is layered monads.


title: Types for Safe Locking

authors:
Cormac Flanagan
Martín Abadi


title: Types and Subtypes for Client-Server Interactions

authors:
Simon J. Gay
Malcolm Hole


title: Functional Reactive Programming (Abstract)


title: Polytypic Compact Printing and Parsing

authors:
Patrik Jansson
Johan Jeuring


title: Quotienting Share for Dependency Analysis

authors:
Andy King
Jan-Georg Smaus
Patricia M. Hill


title: Expressing Structural Properties as Language Constructs

authors:
Shriram Krishnamurthi
Yan-David Erlich
Matthias Felleisen


title: Dynamic Programming via Static Incrementalization

authors:
Yanhong A. Liu
Scott D. Stoller


title: An Idealized MetaML: Simpler, and More Expressive

authors:
Eugenio Moggi
Walid Taha
Zine-El-Abidine Benaissa
Tim Sheard


title: Type-Based Decompilation (or Program Reconstruction via Type Reconstruction)


title: Interprocedural Control Flow Analysis

authors:
Flemming Nielson
Hanne Riis Nielson


title: Deterministic Expressions in C


title: Set-Based Failure Analysis for Logic Programs and Concurrent Constraint Programs

authors:
Andreas Podelski
Witold Charatonik
Martin Müller


title: A Programming Logic for Sequential Java

authors:
Arnd Poetzsch-Heffter
Peter Müller


title: A Per Model of Secure Information Flow in Sequential Programs

authors:
Andrei Sabelfeld
David Sands


title: Higher-Order Code Splicing


title: Safe and Principled Language Interoperation

authors:
Valery Trifonov
Zhong Shao


title: Faithful Translations between Polyvariant Flows and Polymorphic Types

authors:
Torben Amtoft
Franklyn A. Turbak


title: On the Expressiveness of Event Notification in Data-Driven Coordination Languages

authors:
Nadia Busi
Gianluigi Zavattaro


title: Flow-Directed Closure Conversion for Typed Languages

authors:
Henry Cejtin
Suresh Jagannathan
Stephen Weeks


title: Directional Type Checking for Logic Programs: Beyond Discriminative Types


title: Formalizing Implementation Strategies for First-Class Continuations

abstract:
We present the first formalization of implementation strategies for first-class continuations. The formalization hinges on abstract machines for continuation-passing style (CPS) programs with a special treatment for the current continuation, accounting for the essence of first-class continuations. These abstract machines are proven equivalent to a standard, substitution-based abstract machine. The proof techniques work uniformly for various representations of continuations. As a byproduct, we also present a formal proof of the two folklore theorems that one continuation identifier is enough for second-class continuations and that second-class continuations are stackable.

A large body of work exists on implementing continuations, but it is predominantly empirical and implementation-oriented. In contrast, our formalization abstracts the essence of first-class continuations and provides a uniform setting for specifying and formalizing their representation.


title: Correctness of Java Card Method Lookup via Logical Relations

authors:
Ewen Denney
Thomas P. Jensen


title: Compile-Time Debugging of C Programs Working on Trees

authors:
Jacob Elgaard
Anders Møller
Michael I. Schwartzbach


title: A Calculus for Compiling and Linking Classes

authors:
Kathleen Fisher
John H. Reppy
Jon G. Riecke


title: Abstract Domains for Universal and Existential Properties

authors:
Andrew Heaton
Patricia M. Hill
Andy King


title: A Type System for Bounded Space and Functional In-Place Update--Extended Abstract


title: Secure Information Flow as Typed Process Behaviour

authors:
Kohei Honda
Vasco Thudichum Vasconcelos
Nobuko Yoshida


title: Implementing Groundness Analysis with Definite Boolean Functions

authors:
Jacob M. Howe
Andy King


title: The Correctness of Type Specialisation


title: Type Classes with Functional Dependencies


title: Sharing Continuations: Proofnets for Languages with Explicit Control

authors:
Julia L. Lawall
Harry G. Mairson


title: A Calculus for Link-Time Compilation

authors:
Elena Machkasova
Franklyn A. Turbak


title: Improving the Representation of Infinite Trees to Deal with Sets of Trees


title: On the Translation of Procedures to Finite Machines

authors:
Markus Müller-Olm
Andreas Wolf


title: A Kleene Analysis of Mobile Ambients

authors:
Flemming Nielson
Hanne Riis Nielson
Shmuel Sagiv


title: Functional Nets

abstract: Functional nets combine key ideas of functional programming and Petri nets to yield a simple and general programming notation. They have their theoretical foundation in Join calculus. This paper presents functional nets, reviews Join calculus, and shows how the two relate.


title: A 3-Part Type Inference Engine


title: First-Class Structures for Standard ML


title: Constraint-Based Inter-Procedural Analysis of Parallel Programs

authors:
Helmut Seidl
Bernhard Steffen


title: Polyvariant Flow Analysis with Constrained Types

authors:
Scott F. Smith
Tiejun Wang


title: Alias Types

authors:
Frederick Smith
David Walker
J. Gregory Morrisett


title: On Exceptions Versus Continuations in the Presence of State


title: Equational Reasoning for Linking with First-Class Primitive Modules

authors:
J. B. Wells
René Vestergaard


title: What Are Polymorphically-Typed Ambients?

authors:
Torben Amtoft
A. J. Kfoury
Santiago M. Pericás-Geertsen


title: Fusion on Languages


title: A Formal Executable Semantics of the JavaCard Platform

authors:
Gilles Barthe
Guillaume Dufay
Line Jakubiec
Bernard P. Serpette
Simão Melo de Sousa


title: Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling

authors:
Annalisa Bossi
Sandro Etalle
Sabina Rossi
Jan-Georg Smaus

abstract:
In logic programming, dynamic scheduling refers to a situation where the selection of the atom in each resolution (computation) step is determined at runtime, as opposed to a fixed selection rule such as the left-to-right one of Prolog. This has applications e.g. in parallel programming. A mechanism to control dynamic scheduling is provided in existing languages in the form of delay declarations.

Input-consuming derivations were introduced to describe dynamic scheduling while abstracting from the technical details. In this paper, we first formalise the relationship between delay declarations and input-consuming derivations, showing in many cases a one-to-one correspondence. Then, we define a model-theoretic semantics for input-consuming derivations of simply-moded programs. Finally, for this class of programs, we provide a necessary and sufficient criterion for termination.


title: The Recursive Record Semantics of Objects Revisited


title: Compiling Problem Specifications into SAT

authors:
Marco Cadoli
Andrea Schaerf


title: A Query Language Based on the Ambient Logic

authors:
Luca Cardelli
Giorgio Ghelli


title: Modeling an Algebraic Stepper

authors:
John Clements
Matthew Flatt
Matthias Felleisen


title: JOIN(X): Constraint-Based Type Inference for the Join-Calculus

authors:
Sylvain Conchon
François Pottier


title: Modular Causality in a Synchronous Stream Language

authors:
Pascal Cuoq
Marc Pouzet


title: The Def-inite Approach to Dependency Analysis

authors:
Samir Genaim
Michael Codish


title: Programming the Web with High-Level Programming Languages

authors:
Paul T. Graunke
Shriram Krishnamurthi
Steve Van Der Hoeven
Matthias Felleisen


title: Modal Transition Systems: A Foundation for Three-Valued Program Analysis

authors:
Michael Huth
Radha Jagadeesan
David A. Schmidt


title: A Formalisation of Java's Exception Mechanism


title: Proof-Directed De-compilation of Low-Level Code

authors:
Shin-ya Katsumata
Atsushi Ohori


title: Tool Demonstration: Finding Duplicated Code Using Program Dependences

authors:
Raghavan Komondoor
Susan Horwitz


title: Semantics and Program Analysis of Computationally Secure Information Flow


title: Probabilistic Polynomial-Time Process Calculus and Security Protocol Analysis


title: Backwards Abstract Interpretation of Probabilistic Programs


title: On the Complexity of Constant Propagation

authors:
Markus Müller-Olm
Oliver Rüthing


title: Control-Flow Analysis in Cubic Time

authors:
Flemming Nielson
Helmut Seidl


title: A Systematic Approach to Static Access Control

authors:
François Pottier
Christian Skalka
Scott F. Smith


title: On the Completeness of Model Checking


title: Entailment with Conditional Equality Constraints

authors:
Zhendong Su
Alexander Aiken


title: Enforcing Safety Properties Using Type Specialization


title: Encoding Intensional Type Analysis


title: Typestate Checking of Machine Code

authors:
Zhichen Xu
Thomas W. Reps
Barton P. Miller


title: Secure Information Flow and CPS

authors:
Steve Zdancewic
Andrew C. Myers


title: Another Type System for In-Place Update

authors:
David Aspinall
Martin Hofmann


title: Soft Concurrent Constraint Programming

authors:
Stefano Bistarelli
Ugo Montanari
Francesca Rossi


title: Finite-Control Mobile Ambients

authors:
Witold Charatonik
Andrew D. Gordon
Jean-Marc Talbot


title: Dependency Analysis of Mobile Systems

abstract: We propose an Abstract Interpretation-based static analysis for automatically detecting the dependencies between the names linked to the agents of a mobile system. We focus our study on the mobile systems written in the ?-calculus. We first refine the standard semantics in order to restore the relation between the names and the agents that have declared them. We then abstract the dependency relations that are always satisfied by the names of the agents of a mobile system. That is to say we will detect which names are always pair-wisely equal and which names have necessarily been declared by the same recursive instance of an agent.


title: Thread-Modular Verification for Shared-Memory Programs

authors:
Cormac Flanagan
Stephen N. Freund
Shaz Qadeer


title: A Theory of Second-Order Trees


title: Asserting the Precision of Floating-Point Computations: A Simple Abstract Interpreter

authors:
Eric Goubault
Matthieu Martel
Sylvie Putot


title: Existential Types for Imperative Languages


title: Mixin Modules in a Call-by-Value Setting

authors:
Tom Hirschowitz
Xavier Leroy


title: Tool Support for Improving Test Coverage


title: An Accumulative Parallel Skeleton for All

authors:
Zhenjiang Hu
Hideya Iwasaki
Masato Takeichi


title: Data Space Oriented Tiling


title: Exceptions, Continuations and Macro-expressiveness


title: Propagation of Roundoff Errors in Finite Precision Computations: A Semantics Approach


title: Programming Languages for Compressing Graphics

authors:
Morgan McGuire
Shriram Krishnamurthi
John F. Hughes


title: Type Checking Systems Code


title: Automatic Complexity Analysis

authors:
Flemming Nielson
Hanne Riis Nielson
Helmut Seidl


title: A Prototype Dependency Calculus


title: A Modular, Extensible Proof Method for Small-Step Flow Analyses

authors:
Mitchell Wand
Galen B. Williamson


title: Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures

authors:
Keith Wansbrough
Michael Norrish
Peter Sewell
Andrei Serjantov


title: Higher-Order Intensional Type Analysis


title: Branching Types

authors:
Joe B. Wells
Christian Haack


title: Correction of Functional Logic Programs

authors:
María Alpuente
Demis Ballis
Francisco J. Correa
Moreno Falaschi


title: Using Controller-Synthesis Techniques to Build Property-Enforcing Layers

authors:
Karine Altisen
Aurélie Clodic
Florence Maraninchi
Éric Rutten


title: Approximate Pruning in Tabled Logic Programming

authors:
Luís Fernando Castro
David Scott Warren


title: A Tail-Recursive Semantics for Stack Inspections

authors:
John Clements
Matthias Felleisen


title: Security Properties: Two Agents Are Sufficient

authors:
Hubert Comon-Lundh
Véronique Cortier


title: Core Formal Molecular Biology

authors:
Vincent Danos
Cosimo Laneve


title: Tagging, Encoding, and Jones Optimality

authors:
Olivier Danvy
Pablo E. Martínez López

abstract:
A partial evaluator is said to be Jones-optimal if the result of specializing a self-interpreter with respect to a source program is textually identical to the source program, modulo renaming. Jones optimality has already been obtained if the self-interpreter is untyped. If the selfinterpreter is typed, however, residual programs are cluttered with type tags. To obtain the original source program, these tags must be removed.

A number of sophisticated solutions have already been proposed. We observe, however, that with a simple representation shift, ordinary partial evaluation is already Jones-optimal, modulo an encoding. The representation shift amounts to reading the type tags as constructors for higherorder abstract syntax. We substantiate our observation by considering a typed self-interpreter whose input syntax is higher-order. Specializing this interpreter with respect to a source program yields a residual program that is textually identical to the source program, modulo renaming.


title: Flexible Models for Dynamic Linking

authors:
Sophia Drossopoulou
Giovanni Lagorio
Susan Eisenbach


title: Programming Type-Safe Program Updates

authors:
Martin Erwig
Deling Ren


title: Automatic Software Model Checking Using CLP


title: Requirements on the Execution of Kahn Process Networks

authors:
Marc Geilen
Twan Basten


title: Goal-Independent Suspension Analysis for Logic Programs with Dynamic Scheduling

authors:
Samir Genaim
Andy King


title: On the Secure Implementation of Security Protocols

authors:
Pablo Giambiagi
Mads Dam


title: A Simple Language for Real-Time Cryptographic Protocol Analysis

authors:
Roberto Gorrieri
Enrico Locatelli
Fabio Martinelli


title: Modeling Web Interactions

authors:
Paul T. Graunke
Robert Bruce Findler
Shriram Krishnamurthi
Matthias Felleisen


title: Type Error Slicing in Implicitly Typed Higher-Order Languages

authors:
Christian Haack
Joe B. Wells


title: Handling Encryption in an Analysis for Secure Information Flow


title: Computer Security from a Programming Language and Static Analysis Perspective


title: Type Inference for a Distributed pi-Calculus


title: What Makes a Cryptographic Protocol Secure? The Evolution of Requirements Specification in Formal Cryptographic Protocol Analysis


title: The Rely-Guarantee Method in Isabelle/HOL


title: Register Allocation by Proof Transformation


title: Correctness of Data Representations Involving Heap Data Structures

authors:
Uday S. Reddy
Hongseok Yang


title: Finite Differencing of Logical Formulas for Static Analysis

authors:
Thomas W. Reps
Shmuel Sagiv
Alexey Loginov


title: Rule Formats for Non Interference


title: Verifying Temporal Heap Properties Specified via Evolution Logic

authors:
Eran Yahav
Thomas W. Reps
Shmuel Sagiv
Reinhard Wilhelm


title: Building Certified Libraries for PCC: Dynamic Storage Allocation

authors:
Dachuan Yu
Nadeem Abdul Hamid
Zhong Shao


title: Just Fast Keying in the Pi Calculus

authors:
Martín Abadi
Bruno Blanchet
Cédric Fournet


title: ULM: A Core Programming Model for Global Computing: (Extended Abstract)


title: Compositional Analysis of Authentication Protocols

authors:
Michele Bugliesi
Riccardo Focardi
Matteo Maffei


title: Extracting a Data Flow Analyser in Constructive Logic

authors:
David Cachera
Thomas P. Jensen
David Pichardie
Vlad Rusu


title: ML-Like Inference for Classifiers

authors:
Cristiano Calcagno
Eugenio Moggi
Walid Taha


title: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types

authors:
Sébastien Carlier
Jeff Polakow
J. B. Wells
A. J. Kfoury


title: From Constraints to Finite Automata to Filtering Algorithms

authors:
Mats Carlsson
Nicolas Beldiceanu


title: Sound and Decidable Type Inference for Functional Dependencies

authors:
Gregory J. Duck
Simon L. Peyton Jones
Peter J. Stuckey
Martin Sulzmann


title: Linear Types for Packet Processing

authors:
Robert Ennals
Richard Sharp
Alan Mycroft


title: A Memoizing Semantics for Functional Logic Languages

authors:
Salvador España Boquera
Vicent Estruch


title: Static Analysis of Digital Filters


title: Functors for Proofs and Programs

authors:
Jean-Christophe Filliâtre
Pierre Letouzey


title: Semantical Analysis of Specification Logic, 3: An Operational Approach


title: Adaptive Pattern Matching on Binary Data

authors:
Per Gustafsson
Konstantinos Sagonas


title: Trust Management in Strand Spaces: A Rely-Guarantee Method

authors:
Joshua D. Guttman
F. Javier Thayer
Jay A. Carlson
Jonathan C. Herzog
John D. Ramsdell
Brian T. Sniffen


title: A Hardest Attacker for Leaking References


title: Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types

authors:
Tom Hirschowitz
Xavier Leroy
J. B. Wells


title: Modal Proofs as Distributed Programs (Extended Abstract)

authors:
Limin Jia
David Walker


title: A Control Flow Analysis for Safe and Boxed Ambients

authors:
Francesca Levi
Chiara Bodei


title: A Dependently Typed Ambient Calculus

authors:
Cédric Lhoussaine
Vladimiro Sassone


title: Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors

abstract: We present a new idea to adapt relational abstract domains to the analysis of IEEE 754-compliant floating-point numbers in order to statically detect, through Abstract Interpretation-based static analyses, potential floating-point run-time exceptions such as overflows or invalid operations. In order to take the non-linearity of rounding into account, expressions are modeled as linear forms with interval coefficients. We show how to extend already existing numerical abstract domains, such as the octagon abstract domain, to efficiently abstract transfer functions based on interval linear forms. We discuss specific fixpoint stabilization techniques and give some experimental results.


title: Resources, Concurrency, and Local Reasoning (Abstract)


title: A Distributed Abstract Machine for Boxed Ambient Calculi

authors:
Andrew Phillips
Nobuko Yoshida
Susan Eisenbach


title: Strong Preservation as Completeness in Abstract Interpretation

authors:
Francesco Ranzato
Francesco Tapparo


title: Canonical Graph Shapes


title: Decidable Analysis of Cryptographic Protocols with Products and Modular Exponentiation


title: Answer Type Polymorphism in Call-by-Name Continuation Passing


title: A Semantic Framework for Designer Transactions

authors:
Jan Vitek
Suresh Jagannathan
Adam Welc
Antony L. Hosking


title: BI Hyperdoctrines and Higher-Order Separation Logic

authors:
Bodil Biering
Lars Birkedal
Noah Torp-Smith


title: Deciding Reachability in Mobile Ambients

authors:
Nadia Busi
Gianluigi Zavattaro


title: Enforcing Resource Bounds via Static Verification of Dynamic Checks

authors:
Ajay Chander
David Espinosa
Nayeem Islam
Peter Lee
George C. Necula


title: Computationally Sound, Automated Proofs for Security Protocols

authors:
Véronique Cortier
Bogdan Warinschi


title: The ASTREÉ Analyzer

authors:
Patrick Cousot
Radhia Cousot
Jérôme Feret
Laurent Mauborgne
Antoine Miné
David Monniaux
Xavier Rival


title: A Type Discipline for Authorization Policies

authors:
Cédric Fournet
Andrew D. Gordon
Sergio Maffeis


title: Adjoining Declassification and Attack Models by Abstract Interpretation

authors:
Roberto Giacobazzi
Isabella Mastroeni


title: Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries

authors:
Romain Janvier
Yassine Lakhnech
Laurent Mazaré


title: Java Jr: Fully Abstract Trace Semantics for a Core Java Language

authors:
Alan Jeffrey
Julian Rathke


title: Analysis of an Electronic Voting Protocol in the Applied Pi Calculus

authors:
Steve Kremer
Mark Ryan


title: Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis

authors:
Oukseh Lee
Hongseok Yang
Kwangkeun Yi


title: Forward Slicing by Conjunctive Partial Deduction and Argument Filtering

authors:
Michael Leuschel
Germán Vidal


title: Determinacy Inference for Logic Programs

authors:
Lunjin Lu
Andy King


title: Instant Polymorphic Type Systems for Mobile Process Calculi: Just Add Reduction Rules and Close

authors:
Henning Makholm
J. B. Wells


title: Trace Partitioning in Abstract Interpretation Based Static Analyzers

authors:
Laurent Mauborgne
Xavier Rival


title: Analysis of Modular Arithmetic

authors:
Markus Müller-Olm
Helmut Seidl


title: Interprocedural Herbrand Equalities

authors:
Markus Müller-Olm
Helmut Seidl
Bernhard Steffen


title: Programming with Explicit Security Policies


title: A Type System Equivalent to a Model Checker

authors:
Mayur Naik
Jens Palsberg


title: Complexity of Subtype Satisfiability over Posets

authors:
Joachim Niehren
Tim Priesnitz
Zhendong Su


title: Summaries for While Programs with Recursion

authors:
Andreas Podelski
Ina Schaefer
Silke Wagner


title: A New Foundation for Control-Dependence and Slicing for Modern Program Structures

authors:
Venkatesh Prasad Ranganath
Torben Amtoft
Anindya Banerjee
Matthew B. Dwyer
John Hatcliff


title: Denotational Semantics for Abadi and Leino's Logic of Objects

authors:
Bernhard Reus
Jan Schwinghammer


title: Subtyping First-Class Polymorphic Components

authors:
João Costa Seco
Luís Caires


title: Bottom-Up beta-Reduction: Uplinks and lambda-DAGs

authors:
Olin Shivers
Mitchell Wand


title: Towards a Type System for Analyzing JavaScript Programs


title: A Design for a Security-Typed Language with Certificate-Based Declassification

authors:
Stephen Tse
Steve Zdancewic


title: Streams with a Bottom in Functional Languages

authors:
Hideki Tsuiki
Keiji Sugihara


title: Asserting Bytecode Safety

authors:
Martin Wildmoser
Tobias Nipkow


title: Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types


title: Flow Locks: Towards a Core Calculus for Dynamic Flow Policies

authors:
Niklas Broberg
David Sands


title: A Basic Contract Language for Web Services

authors:
Samuele Carpineti
Cosimo Laneve


title: Inference of User-Defined Type Qualifiers and Qualifier Rules

authors:
Brian Chin
Shane Markstrum
Todd D. Millstein
Jens Palsberg


title: Size-Change Termination Analysis in k-Bits

authors:
Michael Codish
Vitaly Lagoon
Peter Schachte
Peter J. Stuckey


title: Embedding Dynamic Dataflow in a Call-by-Value Language

authors:
Gregory H. Cooper
Shriram Krishnamurthi


title: Types for Hierarchic Shapes

authors:
Sophia Drossopoulou
David G. Clarke
James Noble


title: Linear Regions Are All You Need

authors:
Matthew Fluet
Greg Morrisett
Amal J. Ahmed


title: Type Safety of Generics for the .NET Common Language Runtime


title: Polymorphic Type Inference for the JNI

authors:
Michael Furr
Jeffrey S. Foster


title: Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions

authors:
Sumit Gulwani
Ashish Tiwari


title: Type-Based Amortised Heap-Space Analysis

authors:
Martin Hofmann
Steffen Jost


title: Pure Pattern Calculus

authors:
C. Barry Jay
Delia Kesner


title: ILC: A Foundation for Automated Reasoning About Pointer Programs

authors:
Limin Jia
David Walker


title: Bisimulations for Untyped Imperative Objects

authors:
Vasileios Koutavas
Mitchell Wand


title: Path Optimization in Programs and Its Application to Debugging

authors:
Akash Lal
Junghee Lim
Marina Polishchuk
Ben Liblit


title: A Verification Methodology for Model Fields

authors:
K. Rustan M. Leino
Peter Müller


title: Coinductive Big-Step Operational Semantics


title: The Weird World of Bi-directional Programming


title: Haskell Is Not Not ML

authors:
Ben Rudiak-Gould
Alan Mycroft
Simon L. Peyton Jones


title: Types for Dynamic Reconfiguration

authors:
João Costa Seco
Luís Caires


title: Approaches to Polymorphism in Classical Sequent Calculus

authors:
Alexander J. Summers
Steffen van Bakel


title: A Typed Assembly Language for Confidentiality

authors:
Dachuan Yu
Nayeem Islam


title: A Consistent Semantics of Self-adjusting Computation

authors:
Umut A. Acar
Matthias Blume
Jacob Donham


title: A Concurrent Calculus with Atomic Transactions

authors:
Lucia Acciai
Michele Boreale
Silvano Dal-Zilio

abstract:
The Software Transactional Memory (STM) model is an original approach for controlling concurrent accesses to resources without the need for explicit lock-based synchronization mechanisms. A key feature of STMis to provide a way to group sequences of read and write actions inside atomic blocks, similar to database transactions, whose whole effect should occur atomically.

In this paper, we investigate STM from a process algebra perspective and define an extension of asynchronous CCS with atomic blocks of actions. We show that the addition of atomic transactions results in a very expressive calculus, enough to easily encode other concurrent primitives such as guarded choice and multiset-synchronization (a la join-calculus). The correctness of our encodings is proved using a suitable notion of bisimulation equivalence. The equivalence is then applied to prove interesting "laws of transactions" and to obtain a simple normal form for transactions.


title: Cost Analysis of Java Bytecode

authors:
Elvira Albert
Puri Arenas
Samir Genaim
Germán Puebla
Damiano Zanardini


title: A Certified Lightweight Non-interference Java Bytecode Verifier

authors:
Gilles Barthe
David Pichardie
Tamara Rezk


title: Small Witnesses for Abstract Interpretation-Based Proofs

authors:
Frédéric Besson
Thomas P. Jensen
Tiphaine Turpin


title: On the Implementation of Construction Functions for Non-free Concrete Data Types

authors:
Frédéric Blanqui
Thérèse Hardin
Pierre Weis

abstract: Many algorithms use concrete data types with some additional invariants. The set of values satisfying the invariants is often a set of representatives for the equivalence classes of some equational theory. For instance, a sorted list is a particular representative wrt commutativity. Theories like associativity, neutral element, idempotence, etc. are also very common. Now, when one wants to combine various invariants, it may be difficult to find the suitable representatives and to efficiently implement the invariants. The preservation of invariants throughout the whole program is even more difficult and error prone. Classically, the programmer solves this problem using a combination of two techniques: the definition of appropriate construction functions for the representatives and the consistent usage of these functions ensured via compiler verifications. The common way of ensuring consistency is to use an abstract data type for the representatives; unfortunately, pattern matching on representatives is lost. A more appealing alternative is to define a concrete data type with private constructors so that both compiler verification and pattern matching on representatives are granted. In this paper, we detail the notion of private data type and study the existence of construction functions. We also describe a prototype, called Moca, that addresses the entire problem of defining concrete data types with invariants: it generates efficient construction functions for the combination of common invariants and builds representatives that belong to a concrete data type with private constructors.


title: A Complete Guide to the Future

authors:
Frank S. de Boer
Dave Clarke
Einar Broch Johnsen


title: CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements

authors:
Maria Grazia Buscemi
Ugo Montanari


title: Structured Communication-Centred Programming for Web Services

authors:
Marco Carbone
Kohei Honda
Nobuko Yoshida


title: The Java Memory Model: Operationally, Denotationally, Axiomatically

authors:
Pietro Cenciarelli
Alexander Knapp
Eleonora Sibilio


title: Dependent Types for Low-Level Programming

authors:
Jeremy Condit
Matthew Harren
Zachary R. Anderson
David Gay
George C. Necula


title: Scalar Outcomes Suffice for Finitary Probabilistic Testing

authors:
Yuxin Deng
Rob J. van Glabbeek
Carroll Morgan
Chenyi Zhang

abstract:
The question of equivalence has long vexed research in concurrency, leading to many different denotational- and bisimulation-based approaches; a breakthrough occurred with the insight that tests expressed within the concurrent framework itself, based on a special "success action", yield equivalences that make only inarguable distinctions.

When probability was added, however, it seemed necessary to extend the testing framework beyond a direct probabilistic generalisation in order to remain useful. An attractive possibility was the extension to multiple success actions that yielded vectors of real-valued outcomes.

Here we prove that such vectors are unnecessary when processes are finitary, that is finitely branching and finite-state: single scalar outcomes are just as powerful. Thus for finitary processes we can retain the original, simpler testing approach and its direct connections to other naturally scalar-valued phenomena.


title: Principal Type Schemes for Modular Programs

authors:
Derek Dreyer
Matthias Blume


title: Multi-language Synchronization

authors:
Robert Ennals
David Gay


title: On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning

authors:
Xinyu Feng
Rodrigo Ferreira
Zhong Shao


title: A Fault Tolerance Bisimulation Proof for Consensus (Extended Abstract)

authors:
Adrian Francalanza
Matthew Hennessy


title: Static Analysis by Policy Iteration on Relational Domains

authors:
Stephane Gaubert
Eric Goubault
Ankur Taly
Sarah Zennou


title: Precise Fixpoint Computation Through Strategy Iteration

authors:
Thomas Gawlitza
Helmut Seidl


title: Computing Procedure Summaries for Interprocedural Analysis

authors:
Sumit Gulwani
Ashish Tiwari


title: Immutable Objects for a Java-Like Language

authors:
Christian Haack
Erik Poll
Jan Schäfer
Aleksy Schubert


title: Probabilistic Anonymity Via Coalgebraic Simulations

authors:
Ichiro Hasuo
Yoshinobu Kawabe


title: Anti-pattern Matching

authors:
Claude Kirchner
Radu Kopetz
Pierre-Etienne Moreau


title: Type Reconstruction for General Refinement Types

authors:
Kenneth L. Knowles
Cormac Flanagan


title: A Rewriting Semantics for Type Inference

authors:
George Kuan
David MacQueen
Robert Bruce Findler


title: A Calculus for Orchestration of Web Services

authors:
Alessandro Lapadula
Rosario Pugliese
Francesco Tiezzi


title: Modal I/O Automata for Interface and Product Line Theories

authors:
Kim Guldstrand Larsen
Ulrik Nyman
Andrzej Wasowski


title: Using History Invariants to Verify Observers

authors:
K. Rustan M. Leino
Wolfram Schulte


title: Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic

authors:
Guodong Li
Scott Owens
Konrad Slind


title: Controlling the What and Where of Declassification in Language-Based Security

authors:
Heiko Mantel
Alexander Reinhard


title: Abstract Predicates and Mutable ADTs in Hoare Type Theory

authors:
Aleksandar Nanevski
Amal Ahmed
Greg Morrisett
Lars Birkedal


title: Techniques for Contextual Equivalence in Higher-Order, Typed Languages


title: Modular Shape Analysis for Dynamically Encapsulated Programs

authors:
Noam Rinetzky
Arnd Poetzsch-Heffter
Ganesan Ramalingam
Mooly Sagiv
Eran Yahav


title: Interprocedurally Analysing Linear Inequality Relations

authors:
Helmut Seidl
Andrea Flexeder
Michael Petter


title: Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts

authors:
Kohei Suenaga
Naoki Kobayashi


title: A Core Calculus for a Comparative Analysis of Bio-inspired Calculi


title: Non-disjunctive Numerical Domain for Array Predicate Abstraction


title: Certificate Translation in Abstract Interpretation

authors:
Gilles Barthe
César Kunz


title: Typing Safe Deallocation


title: A Hybrid Denotational Semantics for Hybrid Systems

authors:
Olivier Bouissou
Matthieu Martel


title: Open Bisimulation for the Concurrent Constraint Pi-Calculus

authors:
Maria Grazia Buscemi
Ugo Montanari


title: Ranking Abstractions

authors:
Aziem Chawdhary
Byron Cook
Sumit Gulwani
Mooly Sagiv
Hongseok Yang


title: Regular Expression Subtyping for XML Query and Update Languages

abstract: XML database query languages such as XQuery employ regular expression types with structural subtyping. Subtyping systems typically have two presentations, which should be equivalent: a declarative version in which the subsumption rule may be used anywhere, and an algorithmic version in which the use of subsumption is limited in order to make typechecking syntax-directed and decidable. However, the XQuery standard type system circumvents this issue by using imprecise typing rules for iteration constructs and defining only algorithmic typechecking, and another extant proposal provides more precise types for iteration constructs but ignores subtyping. In this paper, we consider a core XQuery-like language with a subsumption rule and prove the completeness of algorithmic typechecking; this is straightforward for XQuery proper but requires some care in the presence of more precise iteration typing disciplines. We extend this result to an XML update language we have introduced in earlier work.


title: Tapido: Trust and Authorization Via Provenance and Integrity in Distributed Objects (Extended Abstract)

authors:
Andrew Cirillo
Radha Jagadeesan
Corin Pitcher
James Riely


title: Semi-persistent Data Structures

authors:
Sylvain Conchon
Jean-Christophe Filliâtre


title: Constructive Mathematics and Functional Programming (Abstract)


title: A Formal Implementation of Value Commitment

authors:
Cédric Fournet
Nataliya Guts
Francesco Zappa Nardelli


title: Full Abstraction for Linda

authors:
Cinzia Di Giusto
Maurizio Gabbrielli


title: Cover Algorithms and Their Combination

authors:
Sumit Gulwani
Madan Musuvathi


title: A Theory of Hygienic Macros

authors:
David Herman
Mitchell Wand


title: Oracle Semantics for Concurrent Separation Logic

authors:
Aquinas Hobor
Andrew W. Appel
Francesco Zappa Nardelli


title: Just Forget It - The Semantics and Enforcement of Information Erasure

authors:
Sebastian Hunt
David Sands


title: Linear Declassification

authors:
Yûta Kaneko
Naoki Kobayashi


title: Verification of Equivalent-Results Methods

authors:
K. Rustan M. Leino
Peter Müller


title: Programming in JoCaml (Tool Demonstration)

authors:
Louis Mandel
Luc Maranget


title: Playing with TOY: Constraints and Domain Cooperation

authors:
Sonia Estévez Martín
Antonio J. Fernández
Fernando Sáenz-Pérez


title: Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices!

authors:
Jacob Matthews
Amal Ahmed


title: Upper Adjoints for Fast Inter-procedural Variable Equalities

authors:
Markus Müller-Olm
Helmut Seidl


title: Iterative Specialisation of Horn Clauses

authors:
Christoffer Rosenkilde Nielsen
Flemming Nielson
Hanne Riis Nielson


title: Verification of Higher-Order Computation: A Game-Semantic Approach


title: A Sound Semantics for OCamllight


title: A Realizability Model for Impredicative Hoare Type Theory

authors:
Rasmus Lerchedahl Petersen
Lars Birkedal
Aleksandar Nanevski
Greg Morrisett


title: Practical Programming with Higher-Order Encodings and Dependent Types

authors:
Adam Poswolsky
Carsten Schürmann


title: Inferring Channel Buffer Bounds Via Linear Programming

authors:
Tachio Terauchi
Adam Megacz


title: The Conversation Calculus: A Model of Service-Oriented Computation

authors:
Hugo Torres Vieira
Luís Caires
João Costa Seco


title: Verified, Executable Parsing

authors:
Aditi Barthwal
Michael Norrish


title: Minimization Algorithm for Symbolic Bisimilarity

authors:
Filippo Bonchi
Ugo Montanari


title: Abstract Processes in Orchestration Languages

authors:
Maria Grazia Buscemi
Hernán C. Melgratti


title: Conversation Types

authors:
Luís Caires
Hugo Torres Vieira


title: Existential Quantification for Variant Ownership

authors:
Nicholas Cameron
Sophia Drossopoulou


title: Amortised Memory Analysis Using the Depth of Data Structures


title: An Interval-Based Inference of Variant Parametric Types

authors:
Florin Craciun
Wei-Ngan Chin
Guanhua He
Shengchao Qin


title: All Secrets Great and Small

authors:
Delphine Demange
David Sands


title: Deny-Guarantee Reasoning

authors:
Mike Dodds
Xinyu Feng
Matthew J. Parkinson
Viktor Vafeiadis


title: The Financial Crisis, a Lack of Contract Specification Tools: What Can Finance Learn from Programming Language Design?


title: Abstraction for Concurrent Objects

authors:
Ivana Filipovic
Peter W. O'Hearn
Noam Rinetzky
Hongseok Yang


title: Modular Monad Transformers


title: Type-Based Automated Verification of Authenticity in Cryptographic Protocols

authors:
Daisuke Kikuchi
Naoki Kobayashi


title: Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming

authors:
Matthew R. Lakin
Andrew M. Pitts


title: A Basis for Verifying Multi-threaded Programs

authors:
K. Rustan M. Leino
Peter Müller


title: Is Structural Subtyping Useful? An Empirical Study

authors:
Donna Malayeri
Jonathan Aldrich


title: Global Principal Typing in Partially Commutative Asynchronous Sessions

authors:
Dimitris Mostrous
Nobuko Yoshida
Kohei Honda


title: Handlers of Algebraic Effects

authors:
Gordon D. Plotkin
Matija Pretnar


title: Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services

authors:
Hridesh Rajan
Jia Tao
Steve M. Shaner
Gary T. Leavens


title: Automatic Parallelization with Separation Logic

authors:
Mohammad Raza
Cristiano Calcagno
Philippa Gardner


title: Using Category Theory to Design Programming Languages


title: SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs

authors:
Caitlin Sadowski
Stephen N. Freund
Cormac Flanagan


title: Formalising and Verifying Reference Attribute Grammars in Coq

authors:
Max Schäfer
Torbjörn Ekman
Oege de Moor


title: Exploring the Design Space of Higher-Order Casts

authors:
Jeremy G. Siek
Ronald Garcia
Walid Taha


title: Practical Variable-Arity Polymorphism

authors:
T. Stephen Strickland
Sam Tobin-Hochstadt
Matthias Felleisen


title: A Theory of Non-monotone Memory (Or: Contexts for free)


title: Well-Typed Programs Can't Be Blamed

authors:
Philip Wadler
Robert Bruce Findler


title: An Efficient Algorithm for Solving the Dyck-CFL Reachability Problem on Trees

authors:
Hao Yuan
Patrick Th. Eugster


title: Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis

authors:
Assalé Adjé
Stéphane Gaubert
Eric Goubault


title: Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays

authors:
Torben Amtoft
John Hatcliff
Edwin Rodríguez


title: A Semantic Framework for Declassification and Endorsement

authors:
Aslan Askarov
Andrew C. Myers


title: Amortised Resource Analysis with Separation Logic


title: A PolyTime Functional Language from Light Linear Logic

authors:
Patrick Baillot
Marco Gaboardi
Virgile Mogbil


title: Testing Polymorphic Properties

authors:
Jean-Philippe Bernardy
Patrik Jansson
Koen Claessen


title: Formal Verification of Coalescing Graph-Coloring Register Allocation

authors:
Sandrine Blazy
Benoît Robillard
Andrew W. Appel


title: A Theory of Speculative Computation

authors:
Gérard Boudol
Gustavo Petri


title: Propositional Interpolation and Abstract Interpretation


title: Logical Concurrency Control from Sequential Proofs

authors:
Jyotirmoy V. Deshmukh
G. Ramalingam
Venkatesh Prasad Ranganath
Kapil Vaswani


title: Fluid Updates: Beyond Strong vs. Weak Updates

authors:
Isil Dillig
Thomas Dillig
Alex Aiken


title: Parameterized Memory Models and Concurrent Separation Logic

authors:
Rodrigo Ferreira
Xinyu Feng
Zhong Shao


title: Amortized Resource Analysis with Polynomial Potential

authors:
Jan Hoffmann
Martin Hofmann


title: Generative Operational Semantics for Relaxed Memory Models

authors:
Radha Jagadeesan
Corin Pitcher
James Riely


title: Automating Security Mediation Placement

authors:
Dave King
Susmit Jha
Divya Muthukumaran
Trent Jaeger
Somesh Jha
Sanjit A. Seshia


title: TRX: A Formally Verified Parser Interpreter

authors:
Adam Koprowski
Henri Binsztok


title: Functional Programming in Sublinear Space

authors:
Ugo Dal Lago
Ulrich Schöpp


title: On the Expressive Power of Primitives for Compensation Handling

authors:
Ivan Lanese
Cátia Vaz
Carla Ferreira


title: Separating Shape Graphs

authors:
Vincent Laviron
Bor-Yuh Evan Chang
Xavier Rival


title: Deadlock-Free Channels and Locks

authors:
K. Rustan M. Leino
Peter Müller
Jan Smans


title: The Audacity of Hope: Thoughts on Reclaiming the Database Dream

authors:
Sam Lindley
Philip Wadler


title: Verifying a Compiler for Java Threads


title: A Grammar-Based Approach to Invertible Programs

authors:
Kazutaka Matsuda
Shin-Cheng Mu
Zhenjiang Hu
Masato Takeichi


title: Faulty Logic: Reasoning about Fault Tolerant Programs

authors:
Matthew L. Meola
David Walker


title: A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While

authors:
Keiko Nakata
Tarmo Uustalu


title: Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions

authors:
David A. Naumann
Anindya Banerjee


title: A Universal Calculus for Stream Processing Languages

authors:
Robert Soulé
Martin Hirzel
Robert Grimm
Bugra Gedik
Henrique Andrade
Vibhore Kumar
Kun-Lung Wu


title: Enforcing Stateful Authorization and Information Flow Policies in Fine

authors:
Nikhil Swamy
Juan Chen
Ravi Chugh


title: Stateful Contracts for Affine Types

authors:
Jesse A. Tov
Riccardo Pucella


title: CFA2: A Context-Free Approach to Control-Flow Analysis

authors:
Dimitrios Vardoulakis
Olin Shivers


title: Weighted Dynamic Pushdown Networks


title: Explicit Stabilisation for Modular Rely-Guarantee Reasoning

authors:
John Wickerson
Mike Dodds
Matthew J. Parkinson


title: Verified Software Toolchain - (Invited Talk)


title: Polymorphic Contracts

authors:
João Filipe Belo
Michael Greenberg
Atsushi Igarashi
Benjamin C. Pierce


title: Proving Isolation Properties for Software Transactional Memory

authors:
Annette Bieniusa
Peter Thiemann


title: Typing Copyless Message Passing

authors:
Viviana Bono
Chiara Messa
Luca Padovani


title: Measure Transformer Semantics for Bayesian Machine Learning

authors:
Johannes Borgström
Andrew D. Gordon
Michael Greenberg
James Margetson
Jurgen Van Gael


title: Transfer Function Synthesis without Quantifier Elimination

authors:
Jörg Brauer
Andy King


title: Semantics of Concurrent Revisions

authors:
Sebastian Burckhardt
Daan Leijen


title: Type-Based Access Control in Data-Centric Systems

authors:
Luís Caires
Jorge A. Pérez
João Costa Seco
Hugo Torres Vieira
Lúcio Ferrão


title: Linear Absolute Value Relation Analysis

authors:
Liqian Chen
Antoine Miné
Ji Wang
Patrick Cousot


title: Generalizing the Template Polyhedral Domain

authors:
Michael Colón
Sriram Sankaranarayanan


title: Dataflow Analysis for Datarace-Free Programs

authors:
Arnab De
Deepak D'Souza
Rupesh Nasre


title: Compiling Information-Flow Security to Minimal Trusted Computing Bases

authors:
Cédric Fournet
Jérémy Planul


title: Improving Strategies via SMT Solving

authors:
Thomas Martin Gawlitza
David Monniaux

abstract: We consider the problem of computing numerical invariants of programs by abstract interpretation. Our method eschews two traditional sources of imprecision: (i) the use of widening operators for enforcing convergence within a finite number of iterations (ii) the use of merge operations (often, convex hulls) at the merge points of the control flow graph. It instead computes the least inductive invariant expressible in the domain at a restricted set of program points, and analyzes the rest of the code en bloc. We emphasize that we compute this inductive invariant precisely. For that we extend the strategy improvement algorithm of [Gawlitza and Seidl, 2007]. If we applied their method directly, we would have to solve an exponentially sized system of abstract semantic equations, resulting in memory exhaustion. Instead, we keep the system implicit and discover strategy improvements using SAT modulo real linear arithmetic (SMT). For evaluating strategies we use linear programming. Our algorithm has low polynomial space complexity and performs for contrived examples in the worst case exponentially many strategy improvement steps; this is unsurprising, since we show that the associated abstract reachability problem is Pi-p-2-complete.


title: Typing Local Control and State Using Flow Analysis

authors:
Arjun Guha
Claudiu Saftoiu
Shriram Krishnamurthi


title: Barriers in Concurrent Separation Logic

authors:
Aquinas Hobor
Cristian Gherghina


title: From Exponential to Polynomial-Time Security Typing via Principal Types

authors:
Sebastian Hunt
David Sands


title: Secure the Clones - Static Enforcement of Policies for Secure Object Copying

authors:
Thomas P. Jensen
Florent Kirchner
David Pichardie


title: A New Method for Dependent Parsing

authors:
Trevor Jim
Yitzhak Mandelbaum


title: Biochemical Reaction Rules with Constraints

authors:
Mathias John
Cédric Lhoussaine
Joachim Niehren
Cristian Versari


title: A Testing Theory for a Higher-Order Cryptographic Language - (Extended Abstract)

authors:
Vasileios Koutavas
Matthew Hennessy


title: Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs


title: Algorithmic Nominal Game Semantics

authors:
Andrzej S. Murawski
Nikos Tzevelekos


title: The Relationship between Separation Logic and Implicit Dynamic Frames

authors:
Matthew J. Parkinson
Alexander J. Summers


title: Precise Interprocedural Analysis in the Presence of Pointers to the Stack

authors:
Pascal Sotin
Bertrand Jeannet


title: General Bindings and Alpha-Equivalence in Nominal Isabelle

authors:
Christian Urban
Cezary Kaliszyk


title: What's Decidable about Weak Memory Models?

authors:
Mohamed Faouzi Atig
Ahmed Bouajjani
Sebastian Burckhardt
Madanlal Musuvathi


title: A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert

authors:
Gilles Barthe
Delphine Demange
David Pichardie


title: Concurrent Library Correctness on the TSO Memory Model

authors:
Sebastian Burckhardt
Alexey Gotsman
Madanlal Musuvathi
Hongseok Yang


title: Eventually Consistent Transactions

authors:
Sebastian Burckhardt
Daan Leijen
Manuel Fähndrich
Mooly Sagiv


title: Automated Verification of Equivalence Properties of Cryptographic Protocols

authors:
Rohit Chadha
Stefan Ciobaca
Steve Kremer


title: The Call-by-Need Lambda Calculus, Revisited

authors:
Stephen Chang
Matthias Felleisen

abstract:
The existing call-by-need λ describe lazy evaluation via equational logics. A programmer can use these logics to safely ascertain whether one term is behaviorally equivalent to another or to determine the value of a lazy program. However, neither of the existing calculi models evaluation in a way that matches lazy implementations.

Both calculi suffer from the same two problems. First, the calculi never discard function calls, even after they are completely resolved. Second, the calculi include re-association axioms even though these axioms are merely administrative steps with no counterpart in any implementation.

In this paper, we present an alternative axiomatization of lazy evaluation using a single axiom. It eliminates both the function call retention problem and the extraneous re-association axioms. Our axiom uses a grammar of contexts to describe the exact notion of a needed computation. Like its predecessors, our new calculus satisfies consistency and standardization properties and is thus suitable for reasoning about behavioral equivalence. In addition, we establish a correspondence between our semantics and Launchbury's natural semantics.


title: A Compositional Specification Theory for Component Behaviours

authors:
Taolue Chen
Chris Chilton
Bengt Jonsson
Marta Z. Kwiatkowska


title: Probabilistic Abstract Interpretation

authors:
Patrick Cousot
Michael Monerau


title: Multiparty Session Types Meet Communicating Automata

authors:
Pierre-Malo Deniélou
Nobuko Yoshida


title: Complete Monitors for Behavioral Contracts

authors:
Christos Dimoulas
Sam Tobin-Hochstadt
Matthias Felleisen


title: A Systematic Approach to Delimited Control with Multiple Prompts

authors:
Paul Downen
Zena M. Ariola


title: Generate, Test, and Aggregate - A Calculation-based Framework for Systematic Parallel Programming with MapReduce

authors:
Kento Emoto
Sebastian Fischer
Zhenjiang Hu


title: Trace Spaces: An Efficient New Technique for State-Space Reduction

authors:
Lisbeth Fajstrup
Eric Goubault
Emmanuel Haucourt
Samuel Mimram
Martin Raußen

abstract: State-space reduction techniques, used primarily in model-checkers, all rely on the idea that some actions are independent, hence could be taken in any (respective) order while put in parallel, without changing the semantics. It is thus not necessary to consider all execution paths in the interleaving semantics of a concurrent program, but rather some equivalence classes. The purpose of this paper is to describe a new algorithm to compute such equivalence classes, and a representative per class, which is based on ideas originating in algebraic topology. We introduce a geometric semantics of concurrent languages, where programs are interpreted as directed topological spaces, and study its properties in order to devise an algorithm for computing dihomotopy classes of execution paths. In particular, our algorithm is able to compute a control-flow graph for concurrent programs, possibly containing loops, which is "as reduced as possible" in the sense that it generates traces modulo equivalence. A preliminary implementation was achieved, showing promising results towards efficient methods to analyze concurrent programs, with very promising results compared to partial-order reduction techniques.


title: A Process Algebra for Wireless Mesh Networks

authors:
Ansgar Fehnker
Rob J. van Glabbeek
Peter Höfner
Annabelle McIver
Marius Portmann
Wee Lum Tan

abstract: We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the Ad-hoc On-Demand Distance Vector (AODV) routing protocol and (dis)prove crucial properties such as loop freedom and packet delivery.


title: On the Correctness of the SIMT Execution Model of GPUs

authors:
Axel Habermaier
Alexander Knapp


title: Reasoning about Lock Placements

authors:
Peter Hawkins
Alex Aiken
Kathleen Fisher
Martin C. Rinard
Mooly Sagiv


title: Reasoning about Multi-stage Programs

authors:
Jun Inoue
Walid Taha


title: Fictional Separation Logic

authors:
Jonas Braband Jensen
Lars Birkedal


title: Validating LR(1) Parsers

authors:
Jacques-Henri Jourdan
François Pottier
Xavier Leroy


title: Adding Equations to System F Types

authors:
Neelakantan R. Krishnaswami
Nick Benton


title: GMeta: A Generic Formal Metatheory Framework for First-Order Representations

authors:
Gyesik Lee
Bruno C. d. S. Oliveira
Sungkeun Cho
Kwangkeun Yi


title: Expansion for Universal Quantifiers

authors:
Sergueï Lenglet
Joe B. Wells

abstract:
Expansion is an operation on typings (i.e., pairs of typing environments and result types) defined originally in type systems for the λ-calculus with intersection types in order to obtain principal (i.e., most informative, strongest) typings. In a type inference scenario, expansion allows postponing choices for whether and how to use non-syntax-driven typing rules (e.g., intersection introduction) until enough information has been gathered to make the right decision. Furthermore, these choices can be equivalent to inserting uses of such typing rules at deeply nested positions in a typing derivation, without needing to actually inspect or modify (or even have) the typing derivation. Expansion has in recent years become simpler due to the use of expansion variables (e.g., in System E).

This paper extends expansion and expansion variables to systems with ∀-quantifiers. We present Fs, an extension of System F with expansion, and prove its main properties. This system turns type inference into a constraint solving problem; this could be helpful to design a modular type inference algorithm for System F types in the future.


title: Non-monotonic Self-Adjusting Computation

authors:
Ruy Ley-Wild
Umut A. Acar
Guy E. Blelloch


title: Java and the Java Memory Model - A Unified, Machine-Checked Formalisation


title: A Type and Effect System for Determinism in Multithreaded Programs

authors:
Yi Lu
John Potter
Chenyi Zhang
Jingling Xue


title: Linear Logical Relations for Session-Based Concurrency

authors:
Jorge A. Pérez
Luís Caires
Frank Pfenning
Bernardo Toninho


title: Staged Computation with Staged Lexical Scope


title: Gradual Ownership Types

authors:
Ilya Sergey
Dave Clarke


title: Foundations of C++


title: A Data Driven Approach for Algebraic Loop Invariants

authors:
Rahul Sharma
Saurabh Gupta
Bharath Hariharan
Alex Aiken
Percy Liang
Aditya V. Nori


title: Structural Lock Correlation with Ownership Types

authors:
Yi Lu
John Potter
Jingling Xue


title: Software Verification for Weak Memory via Program Transformation

authors:
Jade Alglave
Daniel Kroening
Vincent Nimal
Michael Tautschnig

abstract: Multiprocessors implement weak memory models, but program verifiers often assume Sequential Consistency (SC), and thus may miss bugs due to weak memory. We propose a sound transformation of the program to verify, enabling SC tools to perform verification w.r.t. weak memory. We present experiments for a broad variety of models (from x86-TSO to Power) and a vast range of verification tools, quantify the additional cost of the transformation and highlight the cases when we can drastically reduce it. Our benchmarks include work-queue management code from PostgreSQL.


title: Slicing-Based Trace Analysis of Rewriting Logic Specifications with iJulienne

authors:
María Alpuente
Demis Ballis
Francisco Frechina
Julia Sapiña


title: Information Reuse for Multi-goal Reachability Analyses

authors:
Dirk Beyer
Andreas Holzer
Michael Tautschnig
Helmut Veith


title: Checking and Enforcing Robustness against TSO

authors:
Ahmed Bouajjani
Egor Derevenetc
Roland Meyer

abstract:
We present algorithms for checking and enforcing robustness of concurrent programs against the Total Store Ordering (TSO) memory model. A program is robust if all its TSO computations correspond to computations under the Sequential Consistency (SC) semantics.

We provide a complete characterization of non-robustness in terms of so-called attacks: a restricted form of (harmful) out-of-program-order executions. Then, we show that detecting attacks can be parallelized, and can be solved using state reachability queries under the SC semantics in a suitably instrumented program obtained by a linear size source-to-source translation. Importantly, the construction is valid for an unbounded number of memory addresses and an arbitrary number of parallel threads. It is independent from the data domain and from the size of store buffers in the TSO semantics. In particular, when the data domain is finite and the number of addresses is fixed, we obtain decidability and complexity results for robustness, even for a parametric number of threads.

As a second contribution, we provide an algorithm for computing an optimal set of fences that enforce robustness. We consider two criteria of optimality: minimization of program size and maximization of its performance. The algorithms we define are implemented, and we successfully applied them to analyzing and correcting several concurrent algorithms.


title: Verifying Concurrent Programs against Sequential Specifications

authors:
Ahmed Bouajjani
Michael Emmi
Constantin Enea
Jad Hamza


title: The Compiler Forest

authors:
Mihai Budiu
Joel Galenson
Gordon D. Plotkin


title: Behavioral Polymorphism and Parametricity in Session-Based Communication

authors:
Luís Caires
Jorge A. Pérez
Frank Pfenning
Bernardo Toninho


title: Laziness by Need


title: Pretty-Big-Step Semantics


title: Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels

authors:
Peter Collingbourne
Alastair F. Donaldson
Jeroen Ketema
Shaz Qadeer


title: Compositional Invariant Checking for Overlaid and Nested Linked Lists

authors:
Constantin Enea
Vlad Saveluc
Mihaela Sighireanu


title: Why3 - Where Programs Meet Provers

authors:
Jean-Christophe Filliâtre
Andrei Paskevich


title: Verifying Concurrent Memory Reclamation Algorithms with Grace

authors:
Alexey Gotsman
Noam Rinetzky
Hongseok Yang


title: Automatic Type Inference for Amortised Heap-Space Analysis

authors:
Martin Hofmann
Dulma Rodriguez


title: Quarantining Weakness - Compositional Reasoning under Relaxed Memory Models (Extended Abstract)

authors:
Radha Jagadeesan
Gustavo Petri
Corin Pitcher
James Riely


title: Language Constructs for Non-Well-Founded Computation

authors:
Jean-Baptiste Jeannin
Dexter Kozen
Alexandra Silva


title: A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness

authors:
Ioannis T. Kassios
Eleftherios Kritikos


title: Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems

authors:
Joost-Pieter Katoen
Doron A. Peled


title: Model-Checking Higher-Order Programs with Recursive Types

authors:
Naoki Kobayashi
Atsushi Igarashi


title: Concurrent Flexible Reversibility

authors:
Ivan Lanese
Michael Lienhardt
Claudio Antares Mezzina
Alan Schmitt
Jean-Bernard Stefani


title: FliPpr: A Prettier Invertible Printing System

authors:
Kazutaka Matsuda
Meng Wang


title: Distributed Electronic Rights in JavaScript

authors:
Mark S. Miller
Tom Van Cutsem
Bill Tulloh

abstract: Contracts enable mutually suspicious parties to cooperate safely through the exchange of rights. Smart contracts are programs whose behavior enforces the terms of the contract. This paper shows how such contracts can be specified elegantly and executed safely, given an appropriate distributed, secure, persistent, and ubiquitous computational fabric. JavaScript provides the ubiquity but must be significantly extended to deal with the other aspects. The first part of this paper is a progress report on our efforts to turn JavaScript into this fabric. To demonstrate the suitability of this design, we describe an escrow exchange contract implemented in 42 lines of JavaScript code.


title: On Distributability in Process Calculi

authors:
Kirstin Peters
Uwe Nestmann
Ursula Goltz


title: GADTs Meet Subtyping

authors:
Gabriel Scherer
Didier Rémy

abstract: While generalized algebraic datatypes (GADTs) are now considered well-understood, adding them to a language with a notion of subtyping comes with a few surprises. What does it mean for a GADT parameter to be covariant? The answer turns out to be quite subtle. It involves fine-grained properties of the subtyping relation that raise interesting design questions. We allow variance annotations in GADT definitions, study their soundness, and present a sound and complete algorithm to check them. Our work may be applied to real-world ML-like languages with explicit subtyping such as OCaml, or to languages with general subtyping constraints.


title: Counterexample-Guided Precondition Inference

authors:
Mohamed Nassim Seghir
Daniel Kroening


title: Modular Reasoning about Separation of Concurrent Data Structures

authors:
Kasper Svendsen
Lars Birkedal
Matthew J. Parkinson


title: Constraining Delimited Control with Contracts

authors:
Asumu Takikawa
T. Stephen Strickland
Sam Tobin-Hochstadt


title: Higher-Order Processes, Functions, and Sessions: A Monadic Integration

authors:
Bernardo Toninho
Luís Caires
Frank Pfenning


title: Abstract Refinement Types

authors:
Niki Vazou
Patrick Maxim Rondon
Ranjit Jhala


title: Ribbon Proofs for Separation Logic

authors:
John Wickerson
Mike Dodds
Matthew J. Parkinson


title: Grounding Synchronous Deterministic Concurrency in Sequential Programming

authors:
Joaquín Aguado
Michael Mendler
Reinhard von Hanxleden
Insa Fuhrmann


title: A Coq Formalization of the Relational Data Model

authors:
Véronique Benzaken
Evelyne Contejean
Stefania Dumbrava


title: Verified Compilation for Shared-Memory C

authors:
Lennart Beringer
Gordon Stewart
Robert Dockins
Andrew W. Appel


title: Resolving Non-determinism in Choreographies

authors:
Laura Bocchi
Hernán C. Melgratti
Emilio Tuosto


title: Model and Proof Generation for Heap-Manipulating Programs

authors:
Martin Brain
Cristina David
Daniel Kroening
Peter Schrammel


title: A Core Quantitative Coeffect Calculus

authors:
Aloïs Brunel
Marco Gaboardi
Damiano Mazza
Steve Zdancewic


title: Overlapping and Order-Independent Patterns - Definitional Equality for All

authors:
Jesper Cockx
Frank Piessens
Dominique Devriese


title: On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi

authors:
Raphaëlle Crubillé
Ugo Dal Lago

abstract: Probabilistic applicative bisimulation is a recently introduced coinductive methodology for program equivalence in a probabilistic, higher-order, setting. In this paper, the technique is applied to a typed, call-by-value, lambda-calculus. Surprisingly, the obtained relation coincides with context equivalence, contrary to what happens when call-by-name evaluation is considered. Even more surprisingly, full-abstraction only holds in a symmetric setting.


title: The Duality of Construction

authors:
Paul Downen
Zena M. Ariola


title: Staged Composition Synthesis

authors:
Boris Düdder
Moritz Martens
Jakob Rehof


title: Targeted Update - Aggressive Memory Abstraction Beyond Common Sense and Its Application on Static Numeric Analysis


title: Local Reasoning for the POSIX File System

authors:
Philippa Gardner
Gian Ntzik
Adam Wright


title: The Network as a Language Construct

authors:
Tony Garnock-Jones
Sam Tobin-Hochstadt
Matthias Felleisen


title: Bounded Linear Types in a Resource Semiring

authors:
Dan R. Ghica
Alex I. Smith


title: Composable Transactional Objects: A Position Paper

authors:
Maurice Herlihy
Eric Koskinen


title: Affine Parallelization of Loops with Run-Time Dependent Bounds from Binaries

authors:
Aparna Kotha
Kapil Anand
Timothy Creech
Khaled Elwazeer
Matthew Smithson
Rajeev Barua


title: Automatic Termination Verification for Higher-Order Functional Programs

authors:
Takuya Kuwahara
Tachio Terauchi
Hiroshi Unno
Naoki Kobayashi


title: Application-Scale Secure Multiparty Computation

authors:
John Launchbury
Dave Archer
Thomas DuBuisson
Eric Mertens


title: A Correspondence between Two Approaches to Interprocedural Analysis in the Presence of Join

authors:
Ravi Mangal
Mayur Naik
Hongseok Yang


title: REAP: Reporting Errors Using Alternative Paths

authors:
João Matos
João Garcia
Paolo Romano


title: Communicating State Transition Systems for Fine-Grained Concurrent Resources

authors:
Aleksandar Nanevski
Ruy Ley-Wild
Ilya Sergey
Germán Andrés Delbianco


title: Verifying an Open Compiler Using Multi-language Semantics

authors:
James T. Perconti
Amal Ahmed


title: Deriving Pretty-Big-Step Semantics from Small-Step Semantics

authors:
Casper Bach Poulsen
Peter D. Mosses


title: An Array-Oriented Language with Static Rank Polymorphism

authors:
Justin Slepak
Olin Shivers
Panagiotis Manolios


title: Impredicative Concurrent Abstract Predicates

authors:
Kasper Svendsen
Lars Birkedal


title: Gradual Typing for Annotated Type Systems

authors:
Peter Thiemann
Luminous Fennell


title: An Abstract Domain to Infer Ordinal-Valued Ranking Functions

authors:
Caterina Urban
Antoine Miné


title: Measurements in Proof Nets as Higher-Order Quantum Circuits

authors:
Akira Yoshimizu
Ichiro Hasuo
Claudia Faggian
Ugo Dal Lago


title: Checking Linearizability of Encapsulated Extended Operations

authors:
Oren Zomer
Guy Golan-Gueta
G. Ramalingam
Mooly Sagiv


title: Automatic Static Cost Analysis for Parallel Programs

authors:
Jan Hoffmann
Zhong Shao


title: The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
Ngo Tuan Phong


title: Spatial Interpolants

authors:
Aws Albarghouthi
Josh Berdine
Byron Cook
Zachary Kincaid

abstract: We propose Splinter, a new technique for proving properties of heap-manipulating programs that marries (1) a new separation logic-based analysis for heap reasoning with (2) an interpolation-based technique for refining heap-shape invariants with data invariants. Splinter is property directed, precise, and produces counterexample traces when a property does not hold. Using the novel notion of spatial interpolants modulo theories, Splinter can infer complex invariants over general recursive predicates, e.g., of the form all elements in a linked list are even or a binary tree is sorted. Furthermore, we treat interpolation as a black box, which gives us the freedom to encode data manipulation in any suitable theory for a given program (e.g., bit vectors, arrays, or linear arithmetic), so that our technique immediately benefits from any future advances in SMT solving and interpolation.


title: The Problem of Programming Language Concurrency Semantics

authors:
Mark Batty
Kayvan Memarian
Kyndylan Nienhuis
Jean Pichon-Pharabod
Peter Sewell

abstract: Despite decades of research, we do not have a satisfactory concurrency semantics for any general-purpose programming language that aims to support concurrent systems code. The Java Memory Model has been shown to be unsound with respect to standard compiler optimisations, while the C/C++11 model is too weak, admitting undesirable thin-air executions.


title: Witnessing (Co)datatypes

authors:
Jasmin Christian Blanchette
Andrei Popescu
Dmitriy Traytel


title: Fine-Grained Detection of Privilege Escalation Attacks on Browser Extensions

authors:
Stefano Calzavara
Michele Bugliesi
Silvia Crafa
Enrico Steffinlongo


title: A Core Calculus for XQuery 3.0 - Combining Navigational and Pattern Matching Approaches

authors:
Giuseppe Castagna
Hyeonseung Im
Kim Nguyen
Véronique Benzaken


title: Segment Abstraction for Worst-Case Execution Time Analysis

authors:
Pavol Cerný
Thomas A. Henzinger
Laura Kovács
Arjun Radhakrishna
Jakob Zwirchmayr


title: Static Analysis of Spreadsheet Applications for Type-Unsafe Operations Detection

authors:
Tie Cheng
Xavier Rival


title: IsoLATE: A Type System for Self-recursion


title: Refinement Types for Incremental Computational Complexity

authors:
Ezgi Çiçek
Deepak Garg
Umut A. Acar


title: Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages

authors:
Arlen Cox
Bor-Yuh Evan Chang
Xavier Rival


title: Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs

authors:
Cristina David
Daniel Kroening
Matt Lewis

abstract: Proving program termination is typically done by finding a well-founded ranking function for the program states. Existing termination provers typically find ranking functions using either linear algebra or templates. As such they are often restricted to finding linear ranking functions over mathematical integers. This class of functions is insufficient for proving termination of many terminating programs, and furthermore a termination argument for a program operating on mathematical integers does not always lead to a termination argument for the same program operating on fixed-width machine integers. We propose a termination analysis able to generate nonlinear, lexicographic ranking functions and nonlinear recurrence sets that are correct for fixed-width machine arithmetic and floating-point arithmetic. Our technique is based on a reduction from program termination to second-order satisfaction. We provide formulations for termination and non-termination in a fragment of second-order logic with restricted quantification which is decidable over finite domains [1]. The resulting technique is a sound and complete analysis for the termination of finite-state programs with fixed-width integers and IEEE floating-point arithmetic.


title: Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs

abstract: This paper shows that it is possible to reason about the safety and termination of programs handling potentially cyclic, singly-linked lists using propositional reasoning even when the safety invariants and termination arguments depend on constraints over the lengths of lists. For this purpose, we propose the theory SLH of singly-linked lists with length, which is able to capture non-trivial interactions between shape and arithmetic. When using the theory of bit-vector arithmetic as background theory, SLH is efficiently decidable via a reduction to SAT. We show the utility of SLH for software verification by using it to express safety invariants and termination arguments for programs manipulating potentially cyclic, singly-linked lists with unrestricted, unspecified sharing. We also provide an implementation of the decision procedure and apply it to check safety and termination proofs for several heap-manipulating programs.


title: A Verified Compiler for Probability Density Functions

authors:
Manuel Eberl
Johannes Hölzl
Tobias Nipkow

abstract: Bhat et al. developed an inductive compiler that computes density functions for probability spaces described by programs in a probabilistic functional language. We implement such a compiler for a modified version of this language within the theorem prover Isabelle and give a formal proof of its soundness w. r. t. the semantics of the source and target language. Together with Isabelle’s code generation for inductive predicates, this yields a fully verified, executable density compiler. The proof is done in two steps: First, an abstract compiler working with abstract functions modelled directly in the theorem prover’s logic is defined and proved sound. Then, this compiler is refined to a concrete version that returns a target-language expression.


title: Analysis of Asynchronous Programs with Event-Based Synchronization

authors:
Michael Emmi
Pierre Ganty
Rupak Majumdar
Fernando Rosa-Velardo


title: Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System

authors:
Burke Fetscher
Koen Claessen
Michal H. Palka
John Hughes
Robert Bruce Findler


title: Inter-procedural Two-Variable Herbrand Equalities

authors:
Stefan Schulze Frielinghaus
Michael Petter
Helmut Seidl


title: Probabilistic Programs as Spreadsheet Queries

authors:
Andrew D. Gordon
Claudio V. Russo
Marcin Szymczak
Johannes Borgström
Nicolas Rolland
Thore Graepel
Daniel Tarlow


title: Composite Replicated Data Types

authors:
Alexey Gotsman
Hongseok Yang


title: A Semantics for Propositions as Sessions

authors:
Sam Lindley
J. Garrett Morris


title: A Theory of Name Resolution

authors:
Pierre Neron
Andrew P. Tolmach
Eelco Visser
Guido Wachsmuth


title: Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs

authors:
Willem Penninckx
Bart Jacobs
Frank Piessens


title: CoLoSL: Concurrent Local Subjective Logic

authors:
Azalea Raad
Jules Villard
Philippa Gardner


title: Binding Structures as an Abstract Data Type


title: Full Reduction in the Face of Absurdity

authors:
Gabriel Scherer
Didier Rémy


title: Type Targeted Testing

authors:
Eric L. Seidel
Niki Vazou
Ranjit Jhala

abstract: We present a new technique called type targeted testing, which translates precise refinement types into comprehensive test-suites. The key insight behind our approach is that through the lens of SMT solvers, refinement types can also be viewed as a high-level, declarative, test generation technique, wherein types are converted to SMT queries whose models can be decoded into concrete program inputs. Our approach enables the systematic and exhaustive testing of implementations from high-level declarative specifications, and furthermore, provides a gradual path from testing to full verification. We have implemented our approach as a Haskell testing tool called TARGET, and present an evaluation that shows how TARGET can be used to test a wide variety of properties and how it compares against state-of-the-art testing approaches.


title: Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity

authors:
Ilya Sergey
Aleksandar Nanevski
Anindya Banerjee

abstract: We present a lightweight approach to Hoare-style specifications for fine-grained concurrency, based on a notion of time-stamped histories that abstractly capture atomic changes in the program state. Our key observation is that histories form a partial commutative monoid, a structure fundamental for representation of concurrent resources. This insight provides us with a unifying mechanism that allows us to treat histories just like heaps in separation logic. For example, both are subject to the same assertion logic and inference rules e.g., the frame rule. Moreover, the notion of ownership transfer, which usually applies to heaps, has an equivalent in histories. It can be used to formally represent helping--an important design pattern for concurrent algorithms whereby one thread can execute code on behalf of another. Specifications in terms of histories naturally abstract away the internal interference, so that sophisticated fine-grained algorithms can be given the same specifications as their simplified coarse-grained counterparts, making them equally convenient for client-side reasoning. We illustrate our approach on a number of examples and validate all of them ini¾?Coq.


title: A Separation Logic for Fictional Sequential Consistency

authors:
Filip Sieczkowski
Kasper Svendsen
Lars Birkedal
Jean Pichon-Pharabod


title: Monotonic References for Efficient Gradual Typing

authors:
Jeremy G. Siek
Michael M. Vitousek
Matteo Cimini
Sam Tobin-Hochstadt
Ronald Garcia


title: Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement

authors:
Tachio Terauchi
Hiroshi Unno


title: Running Probabilistic Programs Backwards

authors:
Neil Toronto
Jay McCarthy
David Van Horn

abstract: Many probabilistic programming languages allow programs to be run under constraints in order to carry out Bayesian inference. Running programs under constraints could enable other uses such as rare event simulation and probabilistic verification—except that all such probabilistic languages are necessarily limited because they are defined or implemented in terms of an impoverished theory of probability. Measure-theoretic probability provides a more general foundation, but its generality makes finding computational content difficult.


title: Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages

authors:
Pedro B. Vasconcelos
Steffen Jost
Mário Florido
Kevin Hammond


title: Regular Programming for Quantitative Properties of Data Streams

authors:
Rajeev Alur
Dana Fisman
Mukund Raghothaman


title: Practical Optional Types for Clojure

authors:
Ambrose Bonnaire-Sergeant
Rowan Davies
Sam Tobin-Hochstadt

abstract:
Typed Clojure is an optional type system for Clojure, a dynamic language in the Lisp family that targets the JVM. Typed Clojure enables Clojure programmers to gain greater confidence in the correctness of their code via static type checking while remaining in the Clojure world, and has acquired significant adoption in the Clojure community. Typed Clojure repurposes Typed Racket's occurrence typing, an approach to statically reasoning about predicate tests, and also includes several new type system features to handle existing Clojure idioms.

In this paper, we describe Typed Clojure and present these type system extensions, focusing on three features widely used in Clojure. First, multimethods provide extensible operations, and their Clojure semantics turns out to have a surprising synergy with the underlying occurrence typing framework. Second, Java interoperability is central to Clojure's mission but introduces challenges such as ubiquitous null; Typed Clojure handles Java interoperability while ensuring the absence of null-pointer exceptions in typed programs. Third, Clojure programmers idiomatically use immutable dictionaries for data structures; Typed Clojure handles this with multiple forms of heterogeneous dictionary types. We provide a formal model of the Typed Clojure type system incorporating these and other features, with a proof of soundness. Additionally, Typed Clojure is now in use by numerous corporations and developers working with Clojure, and we present a quantitative analysis on the use of type system features in two substantial code bases.


title: A Timed Process Algebra for Wireless Networks with an Application in Routing - (Extended Abstract)

authors:
Emile Bres
Rob J. van Glabbeek
Peter Höfner

abstract: This paper proposes a timed process algebra for wireless networks, an extension of the Algebra for Wireless Networks. It combines treatments of local broadcast, conditional unicast and data structures, which are essential features for the modelling of network protocols. In this framework we model and analyse the Ad hoc On-Demand Distance Vector routing protocol, and show that, contrary to claims in the literature, it fails to be loop free. We also present boundary conditions for a fix ensuring that the resulting protocol is indeed loop free.


title: Computing with Semirings and Weak Rig Groupoids

authors:
Jacques Carette
Amr Sabry