Lectures related to Polymorphism in Coq: Data Structures and Functions

Data Abstraction: Modules and Specifications in Coq

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

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.

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.

Coq Workshop: Introduction to Interactive Theorem Proving

Introduces Coq, an interactive theorem assistant based on the Curry-Howard isomorphism.

Big-step semantics: Defining arithmetic expressions and commands

Covers the definition of a simple programming language and its big-step semantics, including arithmetic expressions and imperative commands.

Introduction to Coq: Arithmetic Expressions and Evaluators

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

Hoare Logic: Foundations and Applications

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

Inductive Propositions: Reasoning and Evaluation Techniques

Discusses inductive propositions, their definitions, and applications in reasoning and evaluation techniques in Coq.

Polymorphism and Proofs

Covers parametric polymorphism, lists construction, tuples, generic methods, merge sort, and proving program properties.

Foundations of Scala: Modelling and Type Systems

Covers the foundations of Scala, including modelling recursive types, parameterized types, and variance.

Verifying Programs with Stainless

Explores the verification of programs using Stainless, focusing on functional correctness, proof assistants, and automation of reasoning tasks.

Lambda Calculus and Type Safety: An Overview

Provides an overview of lambda calculus, type safety, and type inference in programming languages.

Subtyping and Polymorphism

Explores subtyping rules, challenges, and its connection to various forms of polymorphism in programming languages.

Functional Programming: Concepts and Implementation

Covers the concepts and implementation of functional programming in Scala, emphasizing functions, immutable data, and data abstraction.

Parameterized Types: Implementation and Inheritance Principles

Covers parameterized types, their implementation, advantages, weaknesses, and the principles of inheritance in programming.

Type Rules: Progress and Preservation

Covers Amyli, a tiny functional language, type rules, and soundness.

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.

Python Programming: List Comprehensions and Higher Order Functions

Explores advanced Python programming concepts, focusing on list comprehensions and higher order functions.

Stainless Verification System Tutorial

Introduces Stainless, an open-source tool for verifying Scala programs, covering language, modeling, verification tips, and inner workings.

Coq: Overview

Introduces Coq and focuses on proving the theorem and_comm step by step.