The standard approach for the problem of writing and checking safety proofs for untrusted code is construction of a type system that distinguishes safe programs. There are two fundamentally different ways to prove correctness of such type systems: syntactic one (when we prove progress and type preservation directly from typing rules) and semantic one (when we use some mathematical model for types). Appel and McAllester suggested a method for building a semantic model based on approximations of the evaluation result for a given number of steps. Unlike other known constructions this semantics doesn't rely on notions from domain theory or recursion theory, so it is easy to implement. At the same time, it can capture non-trivial and useful features, such as recursive types.
In the talk, we will look at the semantic approach for proving type safety and program equivalence by building step-indexing semantics for the lambda calculus with recursive types and (probably) a more realistic language of von Neumann machine instructions.
Speaker: Dmitry Rozplokhas
Andrew W. Appel, David Allen McAllester. An indexed model of recursive types for foundational proof-carrying code. Transactions on Programming Languages and Systems, 2001. https://dl.acm.org/doi/10.1145/504709.504712
The seminar will be held in google meet on Monday October 19 at 17:30 (google meet room: https://meet.google.com/myu-dhmz-gvu)