Related papers: Quadratic type checking for objective type theory
Linear Temporal Logic (LTL) is a widely used specification framework for linear time properties of systems. The standard approach for verifying such properties is by transforming LTL formulae to suitable $\omega$-automata and then applying…
We prove that the existence of finite combinatorial objects such as affine planes, mutually orthogonal Latin squares, and resolvable balanced incomplete block designs can be reformulated as the existence of certain algorithmic reductions…
We design a proof system for propositional classical logic that integrates two languages for Boolean functions: standard conjunction-disjunction-negation and binary decision trees. We give two reasons to do so. The first is…
In this short review we first recall combinatorial or ($0-$dimensional) quantum field theory (QFT). We then give the main idea of a standard QFT method, called the intermediate field method, and we review how to apply this method to a…
We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one system that disallows construction of iterable data, and one,…
This book introduces a temporal type theory, the first of its kind as far as we know. It is based on a standard core, and as such it can be formalized in a proof assistant such as Coq or Lean by adding a number of axioms. Well-known…
We study an untyped lambda calculus with quantum data and classical control. This work stems from previous proposals by Selinger and Valiron and by Van Tonder. We focus on syntax and expressiveness, rather than (denotational) semantics. We…
The paper presents (human-oriented) specification and (pen-and-paper) verification of the square root function. The function implements Newton method and uses a look-up table for initial approximations. Specification is done in terms of…
The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The…
We exhibit a computational type theory which combines the higher-dimensional structure of cartesian cubical type theory with the internal parametricity primitives of parametric type theory, drawing out the similarities and distinctions…
I consider the following generic scenario: an abstract model M of some 'real' system is only partially presented, or partially known to us, and we have to ensure that the actual system satisfies a given specification, formalised in some…
As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. In classical computing, formal verification and sound static type systems prevent several classes…
We describe a resolvent-type method for estimating time integrals of time-dependent functionals of general right processes in equilibrium and apply this result in the case of weakly asymmetric one-dimensional simple exclusion showing a weak…
Refinement types sharpen systems of simple and dependent types by offering expressive means to more precisely classify well-typed terms. We present a system of refinement types for LF in the style of recent formulations where only canonical…
One may formulate the dependent product types of Martin-L\"of type theory either in terms of abstraction and application operators like those for the lambda-calculus; or in terms of introduction and elimination rules like those for the…
Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are quantitative extensions of linear temporal logic, which are prominent and widely used in the verification of real-timed systems. It was recently shown that the…
We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a…
This paper addresses the problem of checking invariant properties for a large class of symbolic transition systems, defined by a combination of SMT theories and quantifiers. State variables can be functions from an uninterpreted sort…
This paper introduces a novel type theory and logic for probabilistic reasoning. Its logic is quantitative, with fuzzy predicates. It includes normalisation and conditioning of states. This conditioning uses a key aspect that distinguishes…
Affine forms are a common way to represent convex sets of $\mathbb{R}$ using a base of error terms $\epsilon \in [-1, 1]^m$. Quadratic forms are an extension of affine forms enabling the use of quadratic error terms $\epsilon_i \epsilon_j$.…