PhD Abstracts
series editor for further details.
26,098 papers · page 209 of 1,305
PhD Abstracts
series editor for further details.
Level-p-complexity of Boolean functions using thinning, memoization, and polynomials
Abstract This paper describes a purely functional library for computing level- p -complexity of Boolean functions and applies it to two-level iterated majority. Boolean functions are simply functions from n bits to one bit, and they can describe digital circuits, voting systems, …
Trace contracts
Abstract Behavioral software contracts allow programmers to strengthen the obligations and promises that they express with conventional types. They lack expressive power, though, when it comes to invariants that hold across several function calls. Trace contracts narrow this expr…
A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic Go
Abstract Featherweight Generic Go (FGG) is a minimal core calculus modeling the essential features of the programming language Go. It includes support for overloaded methods, interface types, structural subtyping, and generics. The most straightforward semantic description of the…
A correct-by-construction conversion from lambda calculus to combinatory logic
Abstract This pearl defines a translation from well-typed lambda terms to combinatory logic, where both the preservation of types and the correctness of the translation are enforced statically.
Contract lenses: Reasoning about bidirectional programs via calculation
Abstract Bidirectional transformations (BXs) are a mechanism for maintaining consistency between multiple representations of related data. The lens framework, which usually constructs BXs from lens combinators, has become the mainstream approach to BX programming because of its m…
Optimization-Aware Compiler-Level Event Profiling
Tracking specific events in a program’s execution, such as object allocation or lock acquisition, is at the heart of dynamic analysis. Despite the apparent simplicity of this task, quantifying these events is challenging due to the presence of compiler optimizations. Profiling pe…
Capturing Types
Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties could be guaranteed if one knew the free variables captured by values. We describe CC < :◻ , a calculus where such captured variables are succinctly repre…
Omnisemantics: Smooth Handling of Nondeterminism
This article gives an in-depth presentation of the omni-big-step and omni-small-step styles of semantic judgments. These styles describe operational semantics by relating starting states to sets of outcomes rather than to individual outcomes. A single derivation of these semantic…
A Model Checker for Operator Precedence Languages
The problem of extending model checking from finite state machines to procedural programs has fostered much research toward the definition of temporal logics for reasoning on context-free structures. The most notable of such results are temporal logics on Nested Words, such as Ca…
The Tortoise and the Hare Algorithm for Finite Lists, Compositionally
In the tortoise-and-hare algorithm, when the fast pointer reaches the end of a finite list, the slow pointer points to the middle of this list. In the early 2000’s, this property was found to make it possible to program a palindrome detector for immutable lists that operates in o…
Focusing on Refinement Typing
We present a logically principled foundation for systematizing, in a way that works with any computational effect and evaluation order, SMT constraint generation seen in refinement type systems for functional programming languages. By carefully combining a focalized variant of ca…
Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models
Automatically verifying multi-threaded programs is difficult because of the vast number of thread interleavings, a problem aggravated by weak memory consistency. Partial orders can help with verification because they can represent many thread interleavings concisely. However, the…
Typed-Untyped Interactions: A Comparative Analysis
The literature presents many strategies for enforcing the integrity of types when typed code interacts with untyped code. This article presents a uniform evaluation framework that characterizes the differences among some major existing semantics for typed–untyped interaction. Typ…
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While promising, this methodology was previously not fully formalized and came w…
A Verified Optimizer for Quantum Circuits
We present voqc , the first verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called sqir , a small quantum intermediate representation, which is deeply embedded in Coq. Optim…
Towards Porting Operating Systems with Program Synthesis
The end of Moore’s Law has ushered in a diversity of hardware not seen in decades. Operating system (OS) (and system software) portability is accordingly becoming increasingly critical. Simultaneously, there has been tremendous progress in program synthesis. We set out to explore…
A Derivative-based Parser Generator for Visibly Pushdown Grammars
In this article, we present a derivative-based, functional recognizer and parser generator for visibly pushdown grammars. The generated parser accepts ambiguous grammars and produces a parse forest containing all valid parse trees for an input string in linear time. Each parse tr…
Optimizing Homomorphic Evaluation Circuits by Program Synthesis and Time-bounded Exhaustive Search
We present a new and general method for optimizing homomorphic evaluation circuits. Although fully homomorphic encryption (FHE) holds the promise of enabling safe and secure third party computation, building FHE applications has been challenging due to their high computational co…