Related papers: Formal Semantics of a Classical-Quantum Language
We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which…
We introduce and investigate a weighted propositional configuration logic over commutative semirings. Our logic is intended to serve as a specification language for software architectures with quantitative features. We prove an efficient…
We introduce hybrid algebras as algebraic semantics for hybrid languages with nominals and, possibly, the satisfaction operator. We establish a duality between hybrid algebras and the descriptive two-sorted general frames of Ten Cate. We…
This paper describes an abstract machine for linguistic formalisms that are based on typed feature structures, such as HPSG. The core design of the abstract machine is given in detail, including the compilation process from a high-level…
We develop a classical propositional logic for reasoning about combinatory logic. We define its syntax, axiomatic system and semantics. The syntax and axiomatic system are presented based on classical propositional logic, with typed…
Debates concerning philosophical grounds for the validity of classical and intuitionistic logics often have the very nature of logical proofs as one of the main points of controversy. The intuitionist advocates for a strict notion of…
We give new proofs of soundness (all representable functions on base types lies in certain complexity classes) for Elementary Affine Logic, LFPL (a language for polytime computation close to realistic functional programming introduced by…
Classical programming languages cannot model essential elements of complex systems such as true random number generation. This paper develops a formal programming language called the lambda-q calculus that addresses the fundamental…
Categorical semantics of type theories are often characterized as structure-preserving functors. This is because in category theory both the syntax and the domain of interpretation are uniformly treated as structured categories, so that we…
In this paper we propose an approach to reasoning about properties of imperative programs. We assume in this context that the meanings of program constructs are described using rules in the natural semantics style with the additional…
We explore the logarithmic terms in the soft theorem in four dimensions by analyzing classical scattering with generic incoming and outgoing states and one loop quantum scattering amplitudes. The classical and quantum results are consistent…
The stabiliser fragment of quantum theory is a foundational building block for quantum error correction and the fault-tolerant compilation of quantum programs. In this article, we develop a sound, universal and complete denotational…
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techniques to reason about higher-order probabilistic programs,…
This paper presents a substructural logic of sequents with very restricted exchange and weakening rules. It is sound with respect to sequences of measurements of a quantic system. A sound and complete semantics is provided. The semantic…
Formal semantics offers a complete and rigorous definition of a language. It is important to define different semantic models for a language and different models serve different purposes. Building equivalence between different semantic…
Describing systems in terms of choices and their resulting costs and rewards offers the promise of freeing algorithm designers and programmers from specifying how those choices should be made; in implementations, the choices can be realized…
We present a semantic framework for the deductive verification of hybrid systems with Isabelle/HOL. It supports reasoning about the temporal evolutions of hybrid programs in the style of differential dynamic logic modelled by flows or…
In recent years we have explored using Haskell alongside a traditional mathematical formalism in our large-enrolment university course on topics including logic and formal languages, aiming to offer our students a programming perspective on…
Quantum computing (QC) represents the future of computing systems, but the tools for reasoning about the quantum model of computation, in which the laws obeyed are those on the quantum mechanical scale, are still a mix of linear algebra and…
This paper describes a methodology for defining an executable abstract interpreter from a formal description of the semantics of a programming language. Our approach is based on Skeletal Semantics and an abstract interpretation of its…