26,098 papers · page 109 of 1,305
Abstract Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit. Since these programs can leverage all the expressive power of high-level class…
Abstract We present a compositional denotational semantics for a functional language with first-class parallel composition and shared-memory operations whose operational semantics follows the Release/Acquire weak memory model (RA). The semantics is formulated in Moggi’s monadic a…
Abstract Bidirectional typing is a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they should be used. Bidirectional typing has…
Abstract We report on the implementation of a generic bidirectional algorithm for dependent type theories, following the proposal of the paper "Generic bidirectional typing for dependent type theories".
Abstract Regular expression (regex) matching is fundamental in many applications, especially in web services. However, matching by backtracking—preferred by most real-world implementations for its practical performance and backward compatibility—can suffer from so-called catastro…
Abstract We extend intersection types to a computational $$\lambda $$ λ -calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections—whereby computational effects appear not only in the operational semantics, but also in the typ…
Abstract Logically constrained term rewriting systems (LCTRSs) are a formalism for program analysis with support for data types that are not (co)inductively defined. Only imperative programs have been considered through the lens of LCTRSs so far since LCTRSs were introduced as a …
Abstract We introduce layering to modal type theory to combine type theory with intensional analysis. In particular, we demonstrate this idea by developing a 2-layered modal type theory. At the core of this type theory (layer 0) is a simply typed $$\lambda $$ λ -calculus with no …
Abstract Graded type systems are a class of type system for fine-grained quantitative reasoning about data-flow in programs. Through the use of resource annotations (or grades), a programmer can express various program properties at the type level, reducing the number of typeable…
Abstract Hyperproperties specify the behavior of a system across multiple executions, and are an important extension of regular temporal properties. So far, such properties have resisted comprehensive treatment by software model-checking approaches such as IC3/PDR, due to the nee…
Abstract Inlining is a crucial optimisation when compiling functional programming languages. This paper describes how we have implemented and verified function inlining and loop specialisation for PureCake, a verified compiler for a Haskell-like (purely functional, lazy) programm…
Abstract Sound static analyses are an important ingredient for compiler optimizations and program verification tools. However, mathematically proving that a static analysis is sound is a difficult task due to two problems. First, soundness proofs relate two complicated program se…
Abstract Dependently typed proof assistant rely crucially on definitional equality, which relates types and terms that are automatically identified in the underlying type theory. This paper extends type theory with definitional functor laws, equations satisfied propositionally by…
Abstract This document describes the Coq formalisation accompanying the paper Definitional Functoriality for Dependent (Sub)Types, more specifically the content of section 4.
Abstract Exception handling is a key feature in modern programming languages. Exceptions can be used to deal with errors, or as a means to control the flow of execution of a program. Since they might unexpectedly terminate a program, unhandled exceptions are a serious safety conc…
Abstract Multiparty session types (MSTs) are a type-based approach to verifying communication protocols, represented as global types in the framework. We present a precise subtyping relation for asynchronous MSTs with communicating state machines (CSMs) as implementation model. W…
Abstract Notions of computation can be modelled by monads. Algebraic effects offer a characterization of monads in terms of algebraic operations and equational axioms, where operations are basic programming features, such as reading or updating the state, and axioms specify obser…
Abstract Universal probabilistic programming languages (PPLs) make it relatively easy to encode and automatically solve statistical inference problems. To solve inference problems, PPL implementations often apply Monte Carlo inference algorithms that rely on execution suspension.…
Abstract Legal expert systems routinely rely on date computations to determine the eligibility of a citizen to social benefits or whether an application has been filed on time. Unfortunately, date arithmetic exhibits many corner cases, which are handled differently from one libra…
Abstract Precondition inference is an important problem with many applications in verification and testing. Finding preconditions can be tricky as programs often have loops and arrays, which necessitates finding quantified inductive invariants. However, existing techniques have l…