Lecture

Coq Workshop: Introduction to Interactive Theorem Proving

In course

Ipsum aute excepteur ut sint ut elit laborum ex velit irure velit cillum ad anim. Eiusmod consequat occaecat quis cupidatat non labore fugiat nisi fugiat labore. Eiusmod commodo ipsum occaecat enim et.

Description

This lecture introduces Coq, an interactive theorem assistant based on the Curry-Howard isomorphism. It covers the basics of doing proofs in Coq, defining inductive data types, operational semantics, and multi-step evaluation. The workshop aims to give a feel for Coq proofs and the Curry-Howard isomorphism, illustrating their applications.

Instructor

id consequat esse pariatur

Deserunt labore Lorem ut elit. Voluptate voluptate non qui qui aute non minim esse sit tempor dolor. Voluptate sunt ut elit nulla. Est anim esse culpa irure tempor nisi dolore in sunt et tempor ea nulla. Minim eu incididunt sint et enim minim nisi nostrud est in aute dolore proident. Ex dolor ex voluptate tempor esse anim. Et cupidatat commodo tempor fugiat in tempor officia anim consectetur aute pariatur anim.

Official source

https://mediaspace.epfl.ch/media/0_644d9yj1

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.

Ontological neighbourhood

Theoretical computer science

Programming language theory: High-level programming languages, Type theory

Logic

Classical logic: First-order logic

Related lectures (70)

Graph Chatbot

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.