Modular Verification of Higher-Order Functional Programs
Abstract elided by the publisher.
976 papers · page 15 of 49
Commutative Semantics for Probabilistic Programming
Abstract elided by the publisher.
Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization
Abstract elided by the publisher.
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a concurrent high-level source language and an implementation that uses low-level shared memory primitives. However, existing log…
Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
Abstract elided by the publisher.
Abstract Specifications for Concurrent Maps
Abstract elided by the publisher.
Regular Programming for Quantitative Properties of Data Streams
Abstract elided by the publisher.
Practical Optional Types for Clojure
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, a…
A Timed Process Algebra for Wireless Networks with an Application in Routing - (Extended 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 f…
Computing with Semirings and Weak Rig Groupoids
Abstract elided by the publisher.
On Hierarchical Communication Topologies in the \pi -calculus
This paper is concerned with the shape invariants satisfied by the communication topology of {\pi}-terms, and the automatic inference of these invariants. A {\pi}-term P is hierarchical if there is a finite forest T such that the communication topology of every term reachable fro…
Call-By-Push-Value from a Linear Logic Point of View
Abstract elided by the publisher.
Visible Type Application
Abstract elided by the publisher.
Automatically Splitting a Two-Stage Lambda Calculus
Abstract elided by the publisher.
Probabilistic NetKAT
Abstract elided by the publisher.
Coordinated Concurrent Programming in Syndicate
Abstract elided by the publisher.
An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages
Abstract elided by the publisher.
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs
This paper presents a wp---style calculus for obtaining bounds on the expected run---time of probabilistic programs. Its application includes determining the possibly infinite expected termination time of a probabilistic program and proving positive almost---sure termination--doe…
Improving Floating-Point Numbers: A Lazy Approach to Adaptive Accuracy Refinement for Numerical Computations
Abstract elided by the publisher.
Needle & Knot: Binder Boilerplate Tied Up
Abstract elided by the publisher.