Formal semantics

Related lectures (23)

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

Semantics in Computer Language Processing: Understanding Meaning

Covers the semantics of programming languages, focusing on the Add language and the role of rewriting rules and CK machines in understanding meaning.

Lambda Calculus: Syntax and Abstractions

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

Lambda Calculus: Operational Semantics and Evaluation Strategies

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

Functional Programming: Concepts and Implementation

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

Coq Workshop: Introduction to Interactive Theorem Proving

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

Music Semantics: Problems and Prospects

Explores music semantics, discussing inferences triggered by different musical elements and proposing a framework for understanding music's meaning.

Type Checking and Reconstruction: Equations and Unification

Delves into type checking, reconstruction, equations, unification, Hindley/Milner system, polymorphism, and principal types.

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.

Loop Semantics Example

Explores loop semantics, demonstrating how to systematically compute the meaning of a while loop.

Relational Semantics of Loops

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

Encoding Recursion as Self-Application

Explores lambda calculus, higher-order functions, and recursive function encoding.

Dependent Types in Programming Languages

Explores maps, type operators, equivalence, first-class types, System Fw, Coq, and the challenges of type checking in programming languages.

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.

Operational Semantics: Amyli Language

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

High-Level Synthesis: Formally Verified Elastic Circuits

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

Lambda Calculus and Type Safety: An Overview Log in to Mediaspace to watch this video

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

Hoare Logic: Foundations and Applications Log in to Mediaspace to watch this video

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

Polymorphism in Coq: Data Structures and Functions Log in to Mediaspace to watch this video

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