Lambda JS à la Carte
summary
Presents a modular mechanization of JavaScript semantics using the Coq à la Carte approach to avoid monolithic encodings. It addresses the maintenance and expression-problem difficulties of mechanizing complex languages by enabling reuse and extension of proofs and semantics when adding new JavaScript features, demonstrated on modern JavaScript.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 1:14JS formalization challenges
- 2:38Expression problem in mechanized langs
- 3:21Encoding types for extensibility
- 4:02Functions and functors
- 5:08Fixpoint operator limits
- 6:09Metaprogramming to avoid falsehood
- 7:15Comparing modular mechanization
- 7:57Lambda JS goals
- 9:06Automating composition
- 9:28Extensions with functors
- 10:59Implemented features
- 12:22Future work
- 13:08Summary
- 13:49Q&A: Reduction
- 14:32Q&A: Language evolution
- 14:55Q&A: Teaching JS
- 16:00Q&A
related talks
49mGoing Functional with JS
27mBuilding functional Front-ends with ClojureScript
26mLet's compose JavaScript and Reason
35mAshley Williams - SeattleJS Conference 2017
20mFunctional JavaScript
34mClojureScript: The Essence of Alchemy
53mExplaining Lambda Calculus through Plain JavaScript
30mLearning Functional Programming with JavaScript