Stepindexing semantics of recursive types
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 nontrivial 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 stepindexing semantics for the lambda calculus with recursive types and (probably) a more realistic language of von Neumann machine instructions.
Speaker: Dmitry Rozplokhas
References:
Andrew W. Appel, David Allen McAllester. An indexed model of recursive types for foundational proofcarrying 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/myudhmzgvu)
 About seminars

26 October 2020Representability of invariants of programs with algebraic data type

19 October 2020Stepindexing semantics of recursive types

12 October 2020Incorrectness Logic

5 October 2020Development of domainspecific compilers for specialized processors

28 September 2020Slightly subcubic algorithm for the contextfree language reachability (CFLreachability) problem