Lecture

Polymorphism in Coq: Data Structures and Functions

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.

In courses (2)

CS-428: Interactive theorem proving

A hands-on introduction to interactive theorem proving, computer-checked mathematics, compiler verification, proofs as programs, dependent types, and proof automation. Come learn how to write computer-checked proofs and certified bug-free code! ...

CS-628: Interactive Theorem Proving CS

A hands-on introduction to interactive theorem proving, proofs as programs, dependent types, and to the Coq proof assistant. Come learn how to write bug-free code! ...

Description

This lecture discusses the concept of polymorphism in Coq, focusing on how to model data structures such as lists. The instructor begins by reviewing the previous week's introduction to correctness and program syntax. They then explain how to define inductive types, particularly lists, using type parameters. The lecture covers implicit arguments and custom notations for lists, allowing for more intuitive syntax. The instructor demonstrates how to implement functions on lists, including length, append, and reverse, while addressing common pitfalls in Coq's type system. The importance of structural recursion and proof techniques is emphasized throughout the lecture. The instructor also introduces the concept of axiomatic specifications, highlighting the separation of interface and implementation in proof assistants. The lecture concludes with a discussion on the efficiency of functions and the challenges of proving correctness in Coq, including the distinction between functional and operational semantics. Overall, the lecture provides a comprehensive overview of polymorphism and its application in functional programming within Coq.

Official source

Ontological neighbourhood

Theoretical computer science

Programming language theory: High-level programming languages

Related concepts (32)

Parametric polymorphism

In programming languages and type theory, parametric polymorphism allows a single piece of code to be given a "generic" type, using variables in place of actual types, and then instantiated with particular types as needed. Parametrically polymorphic functions and data types are sometimes called generic functions and generic datatypes, respectively, and they form the basis of generic programming. Parametric polymorphism may be contrasted with ad hoc polymorphism.

Polymorphism (computer science)

In programming language theory and type theory, polymorphism is the provision of a single interface to entities of different types or the use of a single symbol to represent multiple different types. The concept is borrowed from a principle in biology where an organism or species can have many different forms or stages. The most commonly recognized major classes of polymorphism are: Ad hoc polymorphism: defines a common interface for an arbitrary set of individually specified types.

Coq

Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.

Functional programming

In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that map values to other values, rather than a sequence of imperative statements which update the running state of the program. In functional programming, functions are treated as first-class citizens, meaning that they can be bound to names (including local identifiers), passed as arguments, and returned from other functions, just as any other data type can.

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 (46)

Foundations of Software: Modeling Programming Languages

Covers the mathematical study of program behaviors, parsing, domain-specific languages, and powerful tools for language design.

Data Abstraction: Modules and Specifications in Coq

Discusses data abstraction in programming, focusing on modules and specifications in Coq.

Limits and Colimits in Functor Categories

Explores limits and colimits in functor categories, focusing on equalizers, pullbacks, and their significance in category theory.

Inductive Propositions: Understanding Evaluation in Coq

Covers inductive propositions in Coq, focusing on evaluation rules for arithmetic expressions and their applications in defining partial and non-deterministic functions.

Formal Proofs: Checking Invariants and Bounded Model Checking

Explores formal proofs, satisfiability problems, and inductive invariants using SAT queries in sequential circuits.

Related concepts (32)

Parametric polymorphism

Polymorphism (computer science)

Coq

Functional programming

Type system