The Fox and the Hound (Episode 2): Fully Abstract, Robust Compilation and How t
summary
Shows that an identity compiler can be fully abstract yet break a source hyperproperty: a target club symbol context forces termination of a source nonterminating program, so nontermination is not preserved. Gives an abstract framework using syntax and behavior functors, modl maps plus “no internal nondeterminism”, and context functors tied by a natural transformation t. Adds a concrete fix: a target sandbox that blocks the club observable, yielding both full abstraction and robust hyperproperty preservation.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:36What is a secure compiler
- 1:17Fully Abstract Compilation
- 3:15Robust Compilation
- 4:59Fully Abstract vs Robust Compilation
- 7:45Example
- 9:48Best Approach
- 11:37Fully Abstract
- 19:10Howt example
- 20:19Conclusion
related talks
12mFully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
22mA Categorical Basis for Robust Program Analysis
21mSecurely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
19mExtensible Metatheory Mechanization via Family Polymorphism
08mShort Talk: Generalising secure compilation criteria
45mA categorical view of computational effects
31mAbstract your representation and fix your functors