Course

CS-428: Interactive theorem proving

Summary

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!

Lectures

Instructor

Clément Pit-Claudel

Teaching & PhD PhD Students Yawen Guan, Kacper Feliks Korban, Can Cebeci, Alexandre Pinazza, Shardul Chiplunkar Courses Interactive Theorem Proving Project CS-642 A project-focused introduction to interactive theorem proving. Interactive theorem proving CS-428 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 an

Official source

https://edu.epfl.ch/coursebook/en/interactive-theorem-proving-CS-428

Moodle Page

http://go.epfl.ch/CS-428

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

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.

Summary

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!

Lectures

Instructor

Clément Pit-Claudel

Official source

https://edu.epfl.ch/coursebook/en/interactive-theorem-proving-CS-428

Moodle Page

http://go.epfl.ch/CS-428

About this result

Lectures in this course (13)

Introduction to Coq: Arithmetic Expressions and Evaluators

Covers the basics of Coq, focusing on arithmetic expressions, evaluation, and proof techniques.

Polymorphism in Coq: Data Structures and Functions

Covers polymorphism in Coq, focusing on data structures and functions like lists, length, and append.

Data Abstraction: Modules and Specifications in Coq

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

Introduction to Proof Scripting: Basics of Ltac

Introduces the basics of proof scripting in Coq, focusing on the Ltac language and its tactics for managing proofs effectively.

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.

Related courses (32)

CS-452: Foundations of software

The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a program part or a language. Students will learn how to apply ...

CS-214: Software construction

Learn how to design and implement reliable, maintainable, and efficient software using a mix of programming skills (declarative style, higher-order functions, inductive types, parallelism) and fundamental software construction concepts (reusability, abstr ...

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and ...

CS-320: Computer language processing

We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language into machine code using a popular backend called LLVM (htt ...

CS-101: Advanced information, computation, communication I

Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics as diverse as mathematical reasoning, combinatorics, disc ...