Skip to main content
Graph
Search
fr
|
en
Login
Search
All
Categories
Concepts
Courses
Lectures
MOOCs
People
Practice
Publications
Startups
Units
Show all results for
Home
Lecture
Inductive Propositions: Understanding Evaluation in Coq
Graph Chatbot
Related lectures (28)
Previous
Page 2 of 3
Next
Coq Workshop: Inductive Data Types and Proofs
Covers the definition of an inductive data type in Coq and how to build proofs interactively using tactics.
Simply Typed Lambda Calculus: Foundations and Properties
Covers the simply typed lambda calculus, focusing on its syntax, semantics, and type system properties such as progress and preservation.
Verifying Programs with Stainless: How Stainless Works
Explores the inner workings of the Stainless framework, emphasizing verification-aware transformations and dependent type checking.
Untitled
Untitled
Proofs: Logic, Mathematics & Algorithms
Explores proof concepts, techniques, and applications in logic, mathematics, and algorithms.
The Languages of Isabelle: Isar, ML, and Scala
Explores the languages of Isabelle, focusing on Isar, ML, and Scala, covering proof schemes, Natural Deduction rules, inductive definitions, and the LCF approach.
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.
Proofs and Logic: Introduction
Introduces logic, proofs, sets, functions, and algorithms in mathematics and computer science.
Coq: Introduction
Introduces Coq, covering defining propositions, proving theorems, and using tactics.
