Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq
Abstract elided by the publisher.
613 papers · page 3 of 31
TorchProbe: Fuzzing Dynamic Deep Learning Compilers
Abstract elided by the publisher.
What Types Are Needed for Typing Dynamic Objects? A Python-Based Empirical Study
Abstract elided by the publisher.
Compilation Semantics for a Programming Language with Versions
Abstract Programming with versions is a paradigm that allows a program to use multiple versions of a module so that the programmer can selectively use functions from both older and newer versions of a single module. Previous work formalized $$\lambda _{\textrm{VL}}$$ λ VL , a cor…
Proofs as Terms, Terms as Graphs
. Starting from an encoding of untyped λ -terms with sharing, defined using synthetic inference rules based on a focused proof system for Gentzen’s LJ , we introduce the positive λ -calculus, a call-by-value calculus with explicit substitutions. This calculus is closely related t…
Towards a Framework for Developing Verified Assemblers for the ELF Format
Abstract Most of the existing work on verified compilation leaves unverified the translation of assembly programs into binary code in object file formats (e.g., the Executable and Linkable Format or ELF). The challenges of developing verified assemblers come from the intrinsic co…
Decoupling the Ascending and Descending Phases in Abstract Interpretation
Abstract elided by the publisher.
Model-Based Fault Classification for Automotive Software
Intensive testing using model-based approaches is the standard way of demonstrating the correctness of automotive software. Unfortunately, state-of-the-art techniques leave a crucial and labor intensive task to the test engineer: identifying bugs in failing tests. Our contributio…
RHLE: Modular Deductive Verification of Relational ∀ ∃ Properties
Relational program logics are used to prove that a desired relationship holds between the execution of multiple programs. Existing relational program logics have focused on verifying that all runs of a collection of programs do not fall outside a desired set of behaviors. Several…
An Algebraic Theory for Shared-State Concurrency
. We present a monadic denotational semantics for a higher-order programming language with shared-state concurrency, i.e
Novice Type Error Diagnosis with Natural Language Models
Abstract elided by the publisher.
Characterizing Functions Mappable over GADTs
Abstract elided by the publisher.
Inferring Region Types via an Abstract Notion of Environment Transformation
Abstract elided by the publisher.
Automated Temporal Verification for Algebraic Effects
Abstract elided by the publisher.
Applicative Intersection Types
Abstract elided by the publisher.
A Calculus with Recursive Types, Record Concatenation and Subtyping
Abstract elided by the publisher.
Fully Abstract and Robust Compilation: And How to Reconcile the Two, Abstractly
Abstract elided by the publisher.
Solving Not-Substring Constraint withFlat Abstraction
Abstract elided by the publisher.
Adaptable Traces for Program Explanations
Abstract elided by the publisher.
Latent Effects for Reusable Language Components
Abstract elided by the publisher.