Dependently typed languages allow us to state a program’s expected properties and automatically check that they are satisfied at compile time. Yet the implementations of these languages are themselves just software, so can we really trust them? ...

We tackle the problem of checking non-proof-carrying code, i.e. automatically proving type-safety (implying in our type system spatial memory safety) of low-level C code or of machine code resulting from its compilation without modification. This ...

In dependently typed programming languages, quotients can be introduced in two different ways: elements of each equivalence class can be made either propositionally equal, at the cost of having to manipulate those equality proofs, or definitionally equal,...

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 ...$$${}_{}$

Gradual typing supports imprecise types in the type system, allowing incremental migration from untyped code to typed in the same language. Through the gradual typing approach, our ongoing work proposes a new theory based on the Martin-Löf type theory ...

Abstract algebra provides a large hierarchy of properties that a collection of objects can satisfy, such as forming an abelian group or a semiring. These classifications can arranged into a broad and typically acyclic directed graph. This graph ...

Bags are ubiquitous in program verification. They are the means of choice when we want to express that a collection of elements is a rearrangement of another collection. We are working towards an “application proving interface” (API) for finite bags ...

In principle, dependent type theory should provide an ideal foundation for formalizing graded rings, where each grade can be of a different type. However, the power of these foundations leaves a plethora of choices for how to proceed with such a ...

Modern dependently typed languages such as Agda can be used to statically enforce the correctness of programs. However, they still lack the large ecosystem of a more popular language like Haskell. To combine the strength of both approaches, we ...

Datatype-generic programming makes it possible to define a construction once and apply it to a large class of datatypes.

It is often used to avoid code duplication in languages that encourage the definition of custom datatypes, in particular state-of-...

The demand to develop more applications and in a faster way has been increasing over the years. Even non-experienced developers are jumping into the market thanks to low-code development platforms such as OutSystems. OSTRICH, a type-safe rich ...

To avoid compilation errors it is desirable to verify that a compiler is type correct—i.e., given well-typed source code, it always outputs well-typed target code. This can be done intrinsically by implementing it as a function in a dependently typed ...

Formal models are important tools in the programming language research community. However, such models are full of intricacies and, due to that, they are subject to subtle errors. Such failures motivated the usage of tools to ensure the correctness of ...

Dependent types have proven a useful technique for development of verified software. Despite the existence of many systems based in dependent type theory, mostly interactive theorem provers but also programming languages, there is no system that ...

Hybrid games combine discrete, continuous, and adversarial dynamics. Differential game logic ([inline-graphic not available: see fulltext]) enables proving (classical) existence of winning strategies. We introduce constructive differential game ...

A liquid type is an ordinary Hindley-Milner type annotated with a logical predicate that states the properties satisfied by the elements of that type. Liquid types are a powerful tool for program verification, as programmers can use them to specify pre- ...

Agda's standard library struggles in various places with n-ary functions and relations. It introduces congruence and substitution operators for functions of arities one and two, and provides users with convenient combinators for manipulating indexed ...

Modern parallel hardware promises unprecedented performance, for the gifted few experts who can program it correctly. Code generators from high-level languages provide an attractive alternative, promising to deliver high performance automatically.

...

Dependent types are a key feature of the proof assistants based on the Curry-Howard isomorphism. It is well known that this correspondence can be extended to classical logic by enriching the language of proofs with control operators. However, they are ...