We present an infinitary version of Multiplicative Additive Linear Logic (sMALL) that serves as logical foundation for a Calculus of Pure Sessions (CaPS). sMALL is infinitary not only because proof derivations may be infinite, but also because ...

Verifying quantum programs has attracted a lot of interest in recent years. In this paper, we consider the following two categories of termination problems of quantum programs with nondeterminism, namely:

• (termination) Is an input of a program ...

We introduce ghost type theory (GTT) a dependent type theory extended with a new universe for ghost data that can safely be erased when running a program but which is not proof irrelevant like with a universe of (strict) propositions. Instead, ghost data ...

This paper studies the problem of synthesizing (lexicographic) polynomial ranking functions for loops that can be described in polynomial arithmetic over integers and reals. While the analogous ranking function synthesis problem for linear ...

We propose a new language feature for ML-family languages, the ability to selectively unbox certain data constructors, so that their runtime representation gets compiled away to just the identity on their argument. Unboxing must be statically rejected ...

We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a natural ...

We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of non-...

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 ...

In dependent type theory, impredicativity is a powerful logical principle that allows the definition of propositions that quantify over arbitrarily large types, potentially resulting in self-referential propositions. Impredicativity can provide a system ...

A primary concern in mergers and acquisitions is the risk the deal may be cancelled before it is completed. We document that “interim risk” varies asymmetrically with the aggregate market return. Deals tend to be renegotiated when the market rises, but ...

We present ParTypes, a type discipline for parallel programs. The model we have in mind comprises a fixed number of processes running in parallel and communicating via collective operations or point-to-point synchronous message exchanges. A type describes ...

We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition. Then, we show that the expected runtime of a quantum program can ...

Sequential emulation is a semantics-based technique to automatically reduce property checking of distributed systems to the analysis of sequential programs. An automated procedure takes as input a formal specification of a distributed system, a property ...

Building on the recent extension of dependent type theory with a universe of definitionally proof-irrelevant types, we introduce TTobs, a new type theory based on the setoidal interpretation of dependent type theory. TTobs equips every type with an ...

We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking: that is, abstract atomic operations ...

This study provides a comprehensive model of an agent’s behavior in response to multiple sales management instruments, including compensation, recruiting/termination, and training. The model takes into account many of the key elements that constitute a ...

Sentential Calculus with Identity ($\mathsf{SCI}$) is an extension of classical propositional logic, featuring a new connective of identity between formulas. In $\mathsf{SCI}$ two formulas are said to be identical if they share the same denotation. In the semantics of ...$\mathsf{}$$\mathsf{}$$\mathsf{}$

Hardware-software codesign for FPGAs requires flexible and changeable boundaries between hardware and software. Design space exploration is facilitated by expressing programs in a language that can be compiled for both CPU and FPGA execution. Such an ...

Dependently typed programming languages and proof assistants such as Agda and Coq rely on computation to automatically simplify expressions during type checking. To overcome the lack of certain programming primitives or logical principles in those ...

Step-indexed logical relations are an extremely useful technique for building operational-semantics-based models and program logics for realistic, richly-typed programming languages. They have proven to be indispensable for modeling features like higher-...