A Scalable, Correct Time-Stamped Stack
(paper)
by Mike Dodds, Andreas Haas and Christoph M. Kirsch
From Communicating Machines to Graphical Choreographies
(preprint)
by Julien Lange, Emilio Tuosto and Nobuko Yoshida
Equations, contractions, and unique solutions
(paper)
by Davide Sangiorgi
Formal verification of a C static analyzer
(paper)
by Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy and David Pichardie
Space-Efficient Manifest Contracts
(paper | tech report)
by Michael Greenberg
Quantitative Interprocedural Analysis
by Krishnendu Chatterjee, Andreas Pavlogiannis and Yaron Velner
Integrating Linear and Dependent Types
(paper)
by Neel Krishnaswami, Pierre Pradic and Nick Benton
Functors are type refinement systems
(paper)
by Paul-André Melliès, Noam Zeilberger
Safe and Efficient Gradual Typing for TypeScript
(tech report)
by Aseem Rastogi, Nikhil Swamy, Cedric Fournet, Gavin Bierman and Panagiotis Vekris
Sound Modular Verification of C Code Executing in an Unverified Context
(paper)
by Pieter Agten, Bart Jacobs and Frank Piessens
Program Boosting: Program Synthesis via Crowd-Sourcing
(paper)
by Robert A Cochran, Loris D'Antoni, Benjamin Livshits, David Molnar and Margus Veanes
Programming up to Congruence
(paper)
by Vilhelm Sjöberg and Stephanie Weirich
Deep Specifications and Certified Abstraction Layers
(paper | tech report | site)
by Ronghui Gu, Jeremie Koenig, Tahina Ramananandro, Zhong Shao, Newman Wu, Shu-chun Weng, Haozhong Zhang and Yu Guo
A Meta Lambda Calculus with Cross-Level Computation
by Kazunori Tobisawa
Specification Inference Using Context-Free Language Reachability
(paper)
by Osbert Bastani, Saswat Anand, Alex Aiken and Osbert Bastani
Runtime enforcement of security policies on black box reactive programs
(paper)
by Minh Ngo, Fabio Massacci, Dimiter Milushev and Frank Piessens
Faster Algorithms for Algebraic Path Properties in RSMs with Constant Treewidth
(arxiv)
by Krishnendu Chatterjee, Prateesh Goyal, Rasmus Ibsen-Jensen and Andreas Pavlogiannis
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
(paper)
by Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal and Derek Dreyer
DReX: A Declarative Language for Efficiently Computable Regular String Transformations
(draft paper)
by Rajeev Alur, Loris D'Antoni and Mukund Raghothaman
K-Java: A Complete Semantics of Java
(paper)
by Denis Bogdanas and Grigore Rosu
Higher Inductive Types as Homotopy-Initial Algebras
(arxiv)
by Kristina Sojakova
A Calculus for Relaxed Memory
（paper)
by Karl Crary and Michael Sullivan
Compositional CompCert
(paper)
by Gordon Stewart, Lennart Beringer, Santiago Cuellar and Andrew W. Appel
Abstract Symbolic Automata
(draft paper)
by Mila Dalla Preda, Roberto Giacobazzi, Arun Lakhotia and Isabella Mastroeni
Analyzing Program Analyses
by Roberto Giacobazzi, Francesco Logozzo and Francesco Ranzato
Self-Representation in Girard's System U
(paper)
by Matt Brown and Jens Palsberg
Conjugate Hylomorphisms: The Mother of All Structured Recursion Schemes
(draft paper)
by Ralf Hinze, Nicolas Wu and Jeremy Gibbons
Decentralizing SDN Policies
(paper)
by Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv and Sharon Shoham
Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction
(paper)
by Giuseppe Castagna, Kim Nguyen, Zhiwu Xu and Pietro Abate
Principal Type Schemes for Gradual Programs
by Ronald Garcia and Matteo Cimini
Full Abstraction for Signal Flow Graphs
(academia)
by Filippo Bonchi, Pawel Sobocinski and Fabio Zanasi
Dependent Information Flow Types
(paper)
by Luísa Lourenço and Luís Caires
Common compiler optimisations are invalid in the C11 memory model and what we can do about it
(paper)
by Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset and Francesco Zappa Nardelli
Manifest Contracts for Datatypes
by Taro Sekiyama, Yuki Nishida and Atsushi Igarashi
Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks
(paper)
by Hao Tang, Xiaoyin Wang, Lingming Zhang, Bing Xie, Lu Zhang and Hong Mei
Leveraging Weighted Automata to Compositional Reasoning of Probabilistic Programs
by Fei He, Xiaowei Gao, Bow-Yaw Wang and Lijun Zhang
Algebraic effects linearity and quantum programming languages
(paper)
by Sam Staton
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
(arxiv)
by Gilles Barthe, Marco Gaboardi, Emilio Gallego Arias, Justin Hsu, Aaron Roth and Pierre-Yves Strub
Probabilistic Termination
by Luis Maria Ferrer Fioriti and Holger Hermanns
Tractable Refinement Checking for Concurrent Objects
(paper)
by Ahmed Bouajjani, Michael Emmi, Constantin Enea and Jad Hamza
From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification
(paper)
by Adam Chlipala
Ur/Web: A Simple Model for Programming the Web
(paper)
by Adam Chlipala
Differential Privacy: Now it's Getting Personal
(paper | site)
by Hamid Ebadi, David Sands and Gerardo Schneider
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant
(paper)
by Benjamin Delaware, Clément Pit-Claudel, Jason Gross and Adam Chlipala
Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests
(arxiv)
by Damien Pous
Succinct Representation of Concurrent Trace Sets
(paper)
by Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna, Roopsha Samanta and Thorsten Tarrach
Predicting Program Properties from Big Code
(paper | site | tool)
by Veselin Raychev, Martin Vechev and Andreas Krause
On Characterizing the Data Access Complexity of Programs
(arxiv)
by Venmugil Elango, Fabrice Rastello, Louis-Noel Pouchet, J. Ramanujam and P. Sadayappan
A Coalgebraic Decision Procedure for NetKAT
(research report (13 pages))
by Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva and Laure Thompson
Proof Spaces for Unbounded Parallelism
(paper)
by Azadeh Farzan, Zachary Kincaid and Andreas Podelski
The Essence of Hygiene
(preprint)
by Michael D. Adams
Data Parallel String Manipulating Programs
(paper)
by Margus Veanes, Todd Mytkowicz, David Molnar and Ben Livshits