A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking
Abstract elided by the publisher.
613 papers · page 5 of 31
Neural Networks, Secure by Construction - An Exploration of Refinement Types
Abstract elided by the publisher.
Relational Synthesis for Pattern Matching
Abstract elided by the publisher.
Automatically Generating Descriptive Texts in Logging Statements: How Far Are We?
Abstract elided by the publisher.
Syntactically Restricting Bounded Polymorphism for Decidable Subtyping
Abstract elided by the publisher.
Parameterized Synthesis with Safety Properties
Parameterized synthesis offers a solution to the problem of constructing correct and verified controllers for parameterized systems. Such systems occur naturally in practice (e.g., in the form of distributed protocols where the amount of processes is often unknown at design time …
Stack-Driven Program Generation of WebAssembly
Abstract elided by the publisher.
P3: A Profiler Suite for Parallel Applications on the Java Virtual Machine
Abstract elided by the publisher.
Certified Semantics for Relational Programming
We present a formal study of semantics for relational programming language miniKanren. First, we formulate denotational semantics which corresponds to the minimal Herbrand model for definite logic programs. Second, we present operational semantics which models the distinctive fea…
REFINITY to Model and Prove Program Transformation Rules
Abstract elided by the publisher.
A Counterexample-Guided Debugger for Non-recursive Datalog
Abstract elided by the publisher.
Algebraic and Coalgebraic Perspectives on Interaction Laws
Abstract elided by the publisher.
Factorization and Normalization, Essentially
Lambda-calculi come with no fixed evaluation strategy. Different strategies may then be considered, and it is important that they satisfy some abstract rewriting property, such as factorization or normalization theorems. In this paper we provide simple proof techniques for these…
Lightweight Functional Logic Meta-Programming
Abstract elided by the publisher.
J-ReCoVer: Java Reducer Commutativity Verifier
Abstract elided by the publisher.
Simulations in Rank-Based Büchi Automata Complementation
The long search for an optimal complementation construction for Buchi automata climaxed with the work of Schewe, who proposed a worst-case optimal rank-based procedure that generates complements of a size matching the theoretical lower bound of (0.76n)n, modulo a polynomial facto…
Existential Types for Relaxed Noninterference
Information-flow security type systems ensure confidentiality by enforcing noninterference: a program cannot leak private data to public channels. However, in practice, programs need to selectively declassify information about private data. Several approaches have provided a noti…
TxForest: A DSL for Concurrent Filestores
Many systems use ad hoc collections of files and directories to store persistent data. For consumers of this data, the process of properly parsing, using, and updating these filestores using conventional APIs is cumbersome and error-prone. Making matters worse, most filestores ar…
Conflict Abstractions and Shadow Speculation for Optimistic Transactional Objects
Abstract elided by the publisher.
Dissecting Widening: Separating Termination from Information
Abstract elided by the publisher.