Type dépendant

En Informatique et en Logique, un type dépendant est un type qui peut dépendre d'une valeur définie dans le langage typé. Les langages Agda et Gallina (de l'assistant de preuve Coq) sont des exemples de langages à type dépendant. Exemples Les types dépendants permettent par exemple de définir le type des listes à n éléments. Voici un exemple en Coq. Inductive Vect (A: Type): nat -> Type := | nil: Vect A 0 | cons (n: nat) (x: A) (t: Vect A n): Vect A (S n). Ainsi, Vect A n définit les listes à n éléments de type A et nil est une liste à 0 élément, et cons n s t est une liste à n + 1 éléments si t est une liste à n éléments. Catégorie:Logique mathématique Catégorie:Théorie des types Catégorie:Théorie de la démonstration

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we make progress towards a better verification experience in general-purpose programming languages by contributing improvements both to the automated checking and the specification of safety properties in languages combining functional and imperative features. We present our extensions in two parts -- reasoning about shared mutable data, and types as specifications -- both of which ultimately rely on reductions of expressive surface languages to a functional core. Throughout, we instantiate our techniques for the particular example of Scala, a mixed-paradigm language widely-used in industry.The first part shows how to extend a verifier for higher-order functions and immutable data to support imperative programs with shared mutable data. We build upon Stainless, a contract-based verification system that relies on SMT solvers to automatically verify a large fragment of Scala. Our technique extends Stainless to check general heap-manipulating programs against modular specifications in the style of dynamic frames. A novelty of our approach is the translation of imperative function contracts that encodes frame conditions using quantifier-free formulas in first-order logic, instead of relying on quantifiers or on dedicated separation logic reasoning. Our quantifier-free encoding enables SMT solvers to both prove safety and to report counterexamples relative to the semantics of procedure contracts.In the second part we turn to types and type-level programming as an alternative means of specifying correctness properties. While dependent types have been studied extensively for purely-functional languages, we investigate their applications to languages with subtyping and (abstractions of) imperative features. We first study a calculus that provides type-level computation through singleton types and allows abstraction of state and IO through a non-deterministic choice operator. This allows for modelling interactions with existing imprecisely-typed and impure code. Our calculus is formalized and mechanically proven correct using the Coq proof assistant. In addition, we develop a prototypical implementation in the Scala compiler and study typical type-level programming use cases in the Scala ecosystem.

EPFL2022

A Nominal Theory of Objects with Dependent Types

Vincent Cremet, Martin Odersky, Matthias Zenger

We design and study newObj, a calculus and dependent type system forobjects and classes which can have types as members. Type members canbe aliases, abstract types, or new types. The type system can modelthe essential concepts of Java's inner classes as well as virtual typesand family polymorphism found in BETA or gbeta. It can also model mostconcepts of SML-style module systems, including sharing constraintsand higher-order functors, but excluding applicative functors.The type system can thus be used as a basis for unifying conceptsthat so far existed in parallel in advanced object systems and inmodule systems. The technical report presents results on confluenceof the calculus, soundness of the type system, and undecidability oftype checking.

2002

Scaling Language Features for Program Verification

Georg Stefan Schmid

EPFL2022

Scaling Language Features for Program Verification

A Nominal Theory of Objects with Dependent Types

The Essence of Dependent Object Types

Scaling Language Features for Program Verification

The Essence of Dependent Object Types

A Nominal Theory of Objects with Dependent Types