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

30 November 2020СFPQ with allpath query semantics

23 November 2020Efficient Fair Conjunction for StructurallyRecursive Relations

16 November 2020SourceTracking Unification via ContextFree Path Querying

9 November 2020Relational Synthesis for Pattern Matching

2 November 2020Definitional ProofIrrelevance without K