Related papers: Formal Verification of Monad Transformers
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the…
We present a Rocq library for monoidal categories, which includes a decision procedure for proving equality of morphisms as well as notations that make it possible to reason as if they were strict, inferring MacLane isomorphims…
We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF, we use the lifting monad (also known as the partial map…
Given a programming language, can we give a monadic denotational semantics that is stable under language extension? Models containing only a single monad are not stable. Models based on type-and-effect systems, in which there is a monad for…
Containers represent a wide class of type constructions relevant for functional programming and (co)inductive reasoning. Indexed containers generalize this notion to better fit the scope of dependently typed programming. When interpreting…
Despite the vast body of research literature proposing algorithms with formal guarantees, the amount of verifiable code in today's systems remains minimal. This discrepancy stems from the inherent difficulty of verifying code, particularly…
Monads are a useful tool for structuring effectful features of computation such as state, non-determinism, and continuations. In the last decade, several generalisations of monads have been suggested which provide a more fine-grained model…
Sharing of notations and theories across an inheritance hierarchy of mathematical structures, e.g., groups and rings, is important for productivity when formalizing mathematics in proof assistants. The packed classes methodology is a…
We present the general framework of \'Ecalle's moulds in the case of linearization of a formal vector field without and within resonances. We enlighten the power of moulds by their universality, and calculability. We modify then \'Ecalle's…
Extensible variants improve the modularity and expressiveness of programming languages: they allow program functionality to be decomposed into independent blocks, and allow seamless extension of existing code with both new cases of existing…
We give a new presentation of interactive realizability with a more explicit syntax. Interactive realizability is a realizability semantics that extends the Curry-Howard correspondence to (sub-)classical logic, more precisely to first-order…
The concept of_refinement_ in type theory is a way of reconciling the "intrinsic" and the "extrinsic" meanings of types. We begin with a rigorous analysis of this concept, settling on the simple conclusion that the type-theoretic notion of…
Interactive theorem provers based on dependent type theory have the flexibility to support both constructive and classical reasoning. Constructive reasoning is supported natively by dependent type theory and classical reasoning is typically…
Typed operational semantics is a method developed by H. Goguen to prove meta-theoretic properties of type systems. This paper studies the metatheory of a type system with dependent record types, using the approach of typed operational…
We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that a property witnessed in a prior state can be soundly recalled in the current state, provided (1) state evolves according to a…
We propose to use Church encodings in typed lambda-calculi as the basis for an automata-theoretic counterpart of implicit computational complexity, in the same way that monadic second-order logic provides a counterpart to descriptive…
Exact real computation is an alternative to floating-point arithmetic where operations on real numbers are performed exactly, without the introduction of rounding errors. When proving the correctness of an implementation, one can focus…
The universal invariant with respect to a given ribbon Hopf algebra is a tangle invariant that dominates all the Reshetikhin-Turaev invariants built from the representation theory of the algebra. We construct a canonical strict monoidal…
Monadic programming presents a significant challenge for many programmers. In light of category theory, we offer a new perspective on the use of monads in functional programming. This perspective is clarified through numerous examples coded…
We investigate a variant of the fuel-based approach to modeling diverging computation in type theories and use it to abstractly capture the essence of oracle Turing machines. The resulting objects we call continuous machines. We prove that…