Fast BGP Simulation of Large Datacenters
Abstract elided by the publisher.
26,098 papers · page 405 of 1,305
Type-Directed Bounding of Collections in Reactive Programs
Our aim is to statically verify that in a given reactive program, the length of collection variables does not grow beyond a given bound. We propose a scalable type-based technique that checks that each collection variable has a given refinement type that specifies constraints abo…
A Practical Algorithm for Structure Embedding
Abstract elided by the publisher.
Automatic Program Repair Using Formal Verification and Expression Templates
Abstract elided by the publisher.
Effect-Driven Flow Analysis
Abstract elided by the publisher.
Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
Abstract elided by the publisher.
A Decidable Logic for Tree Data-Structures with Measurements
Abstract elided by the publisher.
On the Semantics of Snapshot Isolation
Snapshot isolation (SI) is a standard transactional consistency model used in databases, distributed systems and software transactional memory (STM). It is formally defined both declaratively as an acyclicity axiom, and operationally as a concurrent algorithm with memory bearing …
Program Synthesis with Equivalence Reduction
Abstract elided by the publisher.
Application of Abstract Interpretation to the Automotive Electronic Control System
Abstract elided by the publisher.
On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control
Abstract We compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar’s effect handlers, Filinski’s monadic reflection, and delimited control. This comparison allows a precise discussion about the relative expressiv…
POPLMark reloaded: Mechanizing proofs by logical relations
Abstract We propose a new collection of benchmark problems in mechanizing the metatheory of programming languages, in order to compare and push the state of the art of proof assistants. In particular, we focus on proofs using logical relations (LRs) and propose establishing stron…
A relational logic for higher-order programs
Abstract Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on different inputs. Relational program verification can be used for reasoning about a broad range …
How to find a fake coin
There are n coins, all identical in appearance, one of which may be fake. The fake coin, if it exists, is either lighter or heavier than the fair coins, but it is not known which, nor by how much. Given is a balance with two pans but no weights. Equal number of coins can be place…
A theory of RPC calculi for client-server model
Abstract With multi-tier programming languages, programmers can specify the locations of code to run in order to reduce development efforts for the web-based client–server model where programmers write client and server programs separately and test the multiple programs together.…
Review of "The Haskell School of Music: from Signals to Symphonies, " by Paul Hudak and Donya Quick, Cambridge University Press, 2018
Computer languages for music have a long and interesting history.Music signal processing in particular inspired some early work on dataflow computers, and functional programming concepts are frequently associated with music because of the importance of event sequences and sample …
Folding left and right over Peano numbers
For example, consider the standard powerset function that maps the representation of a set as the list of its elements (in any order and without repetition) to the representation of its powerset:Definition powerset (V : Type) (vs : list V)
Constructive Galois Connections
Abstract Galois connections are a foundational tool for structuring abstraction in semantics, and their use lies at the heart of the theory of abstract interpretation. Yet, mechanization of Galois connections using proof assistants remains limited to restricted modes of use, prev…
The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus
Abstract We exploit the idea of proving properties of an abstract machine by using a corresponding semantic artefact better suited to their proof. The abstract machine is an improved version of Pierre Crégut’s full-reducing Krivine machine KN. The original version works with clos…
How to evaluate the performance of gradual type systems
Abstract A sound gradual type system ensures that untyped components of a program can never break the guarantees of statically typed components. This assurance relies on runtime checks, which in turn impose performance overhead in proportion to the frequency and nature of interac…