Verified Functional Programming: Nicolas Voirol public PhD thesis defense

Related lectures (32)

Page 1 of 4

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

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

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

Explores the inner workings of the Stainless framework, emphasizing verification-aware transformations and dependent type checking.

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

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

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

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

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

Covers the simply typed lambda calculus, focusing on its syntax, semantics, and type system properties such as progress and preservation.