Programming Languages
Beloved Curry--Howard correspondence tells that types are intuitionistic propositions, and in constructive math, a proof of proposition can be seen as some kind of a construction, or witness, conveying the information of the proposition. We…
Incremental computations attempt to exploit input similarities over time, reusing work that is unaffected by input changes. To maximize this reuse in a general-purpose programming setting, programmers need a mechanism to identify dynamic…
Many programming language techniques for incremental computation employ programmer-specified names for cached information. At runtime, each name identifies a "cache location" for a dynamic data value or a sub-computation; in sum, these…
Over the past thirty years, there has been significant progress in developing general-purpose, language-based approaches to incremental computation, which aims to efficiently update the result of a computation when an input is changed. A…
In functional programming languages, the classic form of annotation is a single type constraint on a term. Intersection types add complications: a single term may have to be checked several times against different types, in different…
Intersection and union types denote conjunctions and disjunctions of properties. Using bidirectional typechecking, intersection types are relatively straightforward, but union types present challenges. For union types, we can case-analyze a…
We design and implement Zooid, a domain specific language for certified multiparty communication, embedded in Coq and implemented atop our mechanisation framework of asynchronous multiparty session types (the first of its kind). Zooid…
Differential privacy enables general statistical analysis of data with formal guarantees of privacy protection at the individual level. Tools that assist data analysts with utilizing differential privacy have frequently taken the form of…
Primitive recursion is a mature, well-understood topic in the theory and practice of programming. Yet its dual, primitive corecursion, is underappreciated and still seen as exotic. We aim to put them both on equal footing by giving a…
Our aim here is to illustrate how the benefits of structural corecursion can be found in a broader swath of the programming landscape than previously thought. Beginning from a tutorial on structural corecursion in the total, pure functional…
We present a new framework and associated synthesis algorithms for program synthesis over noisy data, i.e., data that may contain incorrect/corrupted input-output examples. This framework is based on an extension of finite tree automata…
Modern deep neural networks increasingly make use of features such as dynamic control flow, data structures and dynamic tensor shapes. Existing deep learning systems focus on optimizing and executing static neural networks which assume a…
Serverless computing (also known as functions as a service) is a new cloud computing abstraction that makes it easier to write robust, large-scale web services. In serverless computing, programmers write what are called serverless…
Compile-time information flow analysis has been a promising technique for protecting confidentiality and integrity of private data. In the last couple of decades, a large number of information flow security tools in the form of run-time…
Formal verification provides strong guarantees of correctness of software, which are especially important in safety or security critical systems. Hoare logic is a widely used formalism for rigorous verification of software against…
Serializability is a well-understood concurrency control mechanism that eases reasoning about highly-concurrent database programs. Unfortunately, enforcing serializability has a high-performance cost, especially on geographically…
In this article, we introduce a new technique for precision tuning. This problem consists of finding the least data types for numerical values such that the result of the computation satisfies some accuracy requirement. State of the art…
In dependently typed programming, proofs of basic, structural properties can be embedded implicitly into programs and do not need to be written explicitly. Besides saving the effort of writing separate proofs, a most distinguishing and…
We focus on control constructs that allow programmers define actions to be performed when respective conditions are met without requiring the explicit evaluation and testing of conditions as part of an imperative algorithm. Such elements…
Concurrent separation logic is distinguished by transfer of state ownership upon parallel composition and framing. The algebraic structure that underpins ownership transfer is that of partial commutative monoids (PCMs). Extant research…