2,199 papers · page 15 of 110
Emanuele D'Osualdo, Azalea Raad, Viktor Vafeiadis
There is an increasing body of literature proposing new and efficient persistent versions of concurrent data structures ensuring that a consistent state can be recovered after a power failure or a crash. Their correctness is typically stated in terms of durable linearizability (D…
Ria Das, Joshua B. Tenenbaum, Armando Solar-Lezama, Zenna Tavares
We present a new algorithm that synthesizes functional reactive programs from observation data. The key novelty is to iterate between a functional synthesis step, which attempts to generate a transition function over observed states, and an automata synthesis step, which adds any…
Ankush Das, Di Wang, Jan Hoffmann
Session types guarantee that message-passing processes adhere to predefined communication protocols. Prior work on session types has focused on deterministic languages but many message-passing systems, such as Markov chains and randomized distributed algorithms, are probabilistic…
Swaraj Dash, Younesse Kaddar, Hugo Paquet, Sam Staton
We show that streams and lazy data structures are a natural idiom for programming with infinite-dimensional Bayesian methods such as Poisson processes, Gaussian processes, jump processes, Dirichlet processes, and Beta processes. The crucial semantic idea, inspired by developments…
Joel D. Day, Vijay Ganesh, Nathan Grewal, Florin Manea
We investigate properties of strings which are expressible by canonical types of string constraints. Specifically, we consider a landscape of 20 logical theories, whose syntax is built around combinations of four common elements of string constraints: language membership (e.g. fo…
Shuo Ding, Qirun Zhang
Many problems in programming language theory and formal methods are undecidable, so they cannot be solved precisely. Practical techniques for dealing with undecidable problems are often based on decidable approximations. Undecidability implies that those approximations are always…
Azadeh Farzan, Dominik Klumpp, Andreas Podelski
The importance of exploitingcommutativity relationsin verification algorithms for concurrent programs is well-known. They can help simplify the proof and improve the time and space efficiency. This paper studies commutativity relations as a first-class object in the setting of ve…
Kuen-Bang Hou (Favonia), Carlo Angiuli, Reed Mullanix
We present a novel formulation of universe polymorphism in dependent type theory in terms of monads on the category of strict partial orders, and a novel algebraic structure, displacement algebras, on top of which one can implement a generalized form of McBride’s “crude but effec…
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger
Quipper is a functional programming language for quantum computing. Proto-Quipper is a family of languages aiming to provide a formal foundation for Quipper. In this paper, we extend Proto-Quipper-M with a construct called dynamic lifting , which is present in Quipper. By virtue …
Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, Greg Morrisett
Many proofs of interactive cryptographic protocols (e.g., as in Universal Composability) operate by proving the protocol at hand to be observationally equivalent to an idealized specification. While pervasive, formal tool support for observational equivalence of cryptographic pro…
Francesco Gavazzo, Cecilia Di Florio
We introduce a general theory of quantitative and metric rewriting systems, namely systems with a rewriting relation enriched over quantales modelling abstract quantities. We develop theories of abstract and term-based systems, refining cornerstone results of rewriting theory (su…
Cinzia Di Giusto, Davide Ferré, Laetitia Laversa, Étienne Lozes
There is a wide variety of message-passing communication models, ranging from synchronous "rendez-vous" communications to fully asynchronous/out-of-order communications. For large-scale distributed systems, the communication model is determined by the transport layer of the netwo…
Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat
Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin’s bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-…
Yu Gu, Takeshi Tsukada, Hiroshi Unno
Motivated by applications to open program reasoning such as maximal specification inference, this paper studiesoptimal CHC solving, a problem to compute maximal and/or minimal solutions of constrained Horn clauses (CHCs). This problem and its subproblems have been studied in the …
Emmanuel Hainry, Romain Péchoux
We introduce a new noninterference policy to capture the class of functions computable in polynomial time on an object-oriented programming language. This policy makes a clear separation between the standard noninterference techniques for the control flow and the layering propert…
Sebastian Hunt, David Sands, Sandro Stucki
This paper proposes a reconciliation of two different theories of information. The first, originally proposed in a lesser-known work by Claude Shannon (some five years after the publication of his celebrated quantitative theory of communication), describes how the information con…
Jules Jacobs, Stephanie Balzer
Reasoning about concurrent programs is challenging, especially if data is shared among threads. Program correctness can be violated by the presence of data races—whose prevention has been a topic of concern both in research and in practice. The Rust programming language is a prim…
Jules Jacobs, Thorsten Wißmann
Coalgebraic bisimilarity minimization generalizes classical automaton minimization to a large class of automata whose transition structure is specified by a functor, subsuming strong, weighted, and probabilistic bisimilarity. This offers the enticing possibility of turning bisimi…
Jerome Jochems, Eddie Jones, Steven J. Ramsay
The monadic shallow linear (MSL) class is a decidable fragment of first-order Horn clauses that was discovered and rediscovered around the turn of the century, with applications in static analysis and verification. We propose a new class of higher-order Horn constraints which ext…
Konstantinos Kallas, Haoran Zhang, Rajeev Alur, Sebastian Angel, Vincent Liu
While serverless platforms substantially simplify the provisioning, configuration, and management of cloud applications, implementing correct services on top of these platforms can present significant challenges to programmers. For example, serverless infrastructures introduce a …