Abstraction Functions as Types

on YouTube ↗26m

" summary

Encodes abstraction functions inside types by adding a single new proposition (an abstract phase) to univalent dependent type theory, then uses a gluing construction plus two modalities to package concrete implementation, abstract specification and the abstraction map into one hybrid type. Proves a noninterference/modularity theorem, extends to cost via a monadic ceiling (sealing) effect that encodes upper bounds, and ships a Cubical Agda prototype with evaluated artifacts.

AI-written summary · about

" chapters (12)

1. 0:00Abstraction functions as types
2. 1:24Modularity with queue implementations
3. 3:54Abstraction functions in verification
4. 6:39Abstraction functions into types
5. 8:04Abstract phase proposition
6. 10:31Hybrid batched-list queue type
7. 11:15Empty function for hybrid queues
8. 13:02Non-interference and modularity
9. 15:27Modularity for cost analysis
10. 18:56Ceiling effect for cost bounds
11. 19:17Key techniques and contributions
12. 20:47Question and answer session

" related talks

• 57mApplied category theory and abstract algebraGabriel Gonzales · LambdaConf Winter Retreat 2017
• 16mSyntax-Generic Operations, Reflectively Reified (Extended Abstract)Hsiang-Shang Ko, Tzu-Chi Lin · TyDe 2022
• 30mA Graded Modal Dependent Type Theory with a Universe and Erasure, FormalizedNils Anders Danielsson, Andreas Abel, Oskar Eriksson · ICFP 2023
• 11mHigher order AbstractionsStephan Boyer · LambdaConf 2017
• 23mReasoning about types and codeSergei Winitzki · Scale By The Bay 2019
• 52mType Theory and its Meaning ExplanationsJon Sterling · LambdaConf 2015
• 53mIntroduction to Intuitionistic Type TheoryVlad Patryshev · LambdaConf 2015
• 54mCategory Theory Through Functional Programming (part 3/3)Alejandro Serrano · LambdaConf Winter Retreat 2017