Lecture

Refinement Types: Practicality and Soundness

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Description

This lecture explores the practicality and soundness of refinement types, which enhance programming language types with logical predicates for more expressive specifications. The instructor presents Liquid Haskell's refinement types, discussing their practicality, generality, expressiveness, and soundness. The lecture covers topics such as safe indexing, light properties verification, and the verification of deeper specifications like type preservation. Additionally, the lecture delves into the verification of light and deep properties using Liquid Haskell, highlighting the challenges and benefits of using refinement types in program verification.

Official source

Related concepts (32)

Formal verification

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Satisfiability modulo theories

In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality (often disallowing quantifiers).

First-order logic

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable.

Logical truth

Logical truth is one of the most fundamental concepts in logic. Broadly speaking, a logical truth is a statement which is true regardless of the truth or falsity of its constituent propositions. In other words, a logical truth is a statement which is not only true, but one which is true under all interpretations of its logical components (other than its logical constants). Thus, logical truths such as "if p, then p" can be considered tautologies.

Type system

In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type (for example, integer, floating point, string) to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term.

Related lectures (64)

Verified Functional Programming: Nicolas Voirol public PhD thesis defense

Explores verified functional programming, formal verification, SMT solvers, type checking, Scala features, automation, and dependent types.

Verifying Programs with Stainless: Part 2

Focuses on using Stainless for program verification, demonstrating the process of verifying programs and ensuring correctness.

Knowledge Representation: Introduction

Covers knowledge representation in AI, logical inference, and applications in various domains.

Hoare Logic: Foundations and Applications

Covers Hoare Logic, its foundations, applications, and significance in program verification.

Propositional Logic: Basics and Applications