Lectures related to Algebraic semantics (computer science)

Type Rules: Progress and Preservation

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

Foundations of Software

Covers the basics of induction, syntax, abstract vs. concrete syntax, and operational semantics for Booleans.

Hoare Logic: Foundations and Applications

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

Lambda Calculus: Church Numerals

Explores Church numerals, Booleans, pairs, recursion, and behavioral equivalence in Lambda Calculus.

Relational Semantics of Loops

Explores the relational semantics of loops in programs and the mathematical interpretation of loop structures.

Operational Semantics: Amyli Language

Covers the Amyli language, including abstract syntax, program representation, and operational semantics.

An Introduction to Iris: Higher-Order Concurrent Separation Logic

Introduces Iris, a logical framework for reasoning about safety and correctness of concurrent higher-order imperative programs, emphasizing its unique characteristics and applications.

Lambda Calculus: Syntax and Abstractions

Introduces terms, abstractions, applications, and values in the lambda calculus.

Coq Workshop: Introduction to Interactive Theorem Proving

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

Polymorphism in Coq: Data Structures and Functions

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

Lambda Calculus: Operational Semantics and Evaluation Strategies

Covers operational semantics and evaluation strategies in lambda calculus, including redex, alternative evaluation strategies, and Church Booleans.

Data Abstraction: Modules and Specifications in Coq

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

From Tests to Proof

Explores the shift from software testing to formal specifications, highlighting the significance of clear requirements in software engineering.

High-Level Synthesis: Formally Verified Elastic Circuits

Presents the development of a verified high-level synthesis compiler for elastic circuits.

Operational Semantics: Amyli Language

Explores operational semantics and inductively defined relations in the Amyli language.