Lectures related to Type Checking Lab

Lambda Calculus and Type Safety: An Overview

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

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

Verified Functional Programming: Nicolas Voirol public PhD thesis defense

Explores verified functional programming, formal verification, SMT solvers, type checking, Scala features, automation, and dependent types.

Verifying Compiler: Spec# Approach

Explores the Spec# programming system, focusing on a verifying compiler for C# 2.0.

Hoare Logic: Foundations and Applications

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

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.

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.

Tuples: Desugaring and Implementation

Covers the implementation details of tuples in Scala, including desugaring, lexical analysis, parsing, and code generation.

Type Inference

Explores type inference in statically typed languages, using algorithms to assign types to program expressions accurately.

Type Checking and Reconstruction: Equations and Unification

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

Multithreading: Code Generation and Type Checking

Covers multithreading, code generation, and type checking in compiler implementation.

Foundations of Scala: Modelling and Type Systems

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

Records and Variants

Introduces records, variants, evaluation rules, typing rules, aliasing challenges, and benefits in programming languages.

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.

Functional Programming: Concepts and Implementation

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

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.

Types in Lambda Calculus

Covers types in lambda calculus, including defining types, specifying rules, and proving soundness.

Type Rules: Progress and Preservation

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

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.

Class hierarchies: pattern matching

Covers class hierarchies, pattern matching, function values, and function calls in Scala.