Lectures related to Relational Semantics of Loops

Music Semantics: Problems and Prospects

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

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.

Hoare Logic: Foundations and Applications

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

Lambda Calculus and Type Safety: An Overview

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

Foundations of Software

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

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.

Loop Semantics Example

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

Type Rules: Progress and Preservation

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

Quantifier Elimination Steps for Presburger Arithmetic

Covers quantifier elimination in Presburger Arithmetic, exposing variables, ensuring coefficients, and handling bounds.

Second Order Logic: WS1S and HOL

Explores Second Order Logic, WS1S, HOL, decision procedures, atomic and composite formulas, and the combination of WS1S with MONA in HOL.

Concurrency Semantics and Verification

Explores concurrency semantics, recursive functions, loops, interleaving modeling, and interpreter verification.

Lambda Calculus: Church Numerals

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

Monotonicity and Semantics of Local Variables

Explores properties of relations, monotonicity, semantics of local variables, and translation in programs.

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.

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.

Automating First-Order Logic Proofs Using Resolution

Covers first-order logic syntax, semantics, Skolemization, resolution, and normal form transformations.

Variables & Operators

Covers the basics of C programming, including variables, operators, and system-oriented programming, emphasizing differences from Java.

Presburger Arithmetic and Quantifier Elimination

Covers Presburger arithmetic, quantifier elimination, and the transformation of formulas into disjunctive normal form.

Inductive Propositions: Reasoning and Evaluation Techniques

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