| 9. 10. 2024 | Take-aways from using Deduce in the classroom – siek.blogspot.com
|
| 11. 8. 2024 | Binary Search Trees, Correctly! – siek.blogspot.com
|
| 20. 7. 2024 | Binary Trees with In-order Iterators (Part 2) – siek.blogspot.com
|
| 18. 7. 2024 | Binary Trees with In-order Iterators (Part 1) – siek.blogspot.com
|
| 30. 6. 2024 | Merge Sort with Leftovers, Correctly – siek.blogspot.com
|
| 18. 6. 2024 | Sequential Search, Correctly – siek.blogspot.com
|
| 17. 6. 2024 | Data Structures and Algorithms, Correctly – siek.blogspot.com
|
| 17. 6. 2024 | Insertion Sort, Correctly – siek.blogspot.com
|
| 8. 6. 2023 | Help! We're Failing to Prove Correctness of Closure Conversion using Denotational Semantics (Graph Models) – siek.blogspot.com
|
| 17. 5. 2023 | Gradual Guarantee via Step-indexed Logical Relations – siek.blogspot.com
|
| 18. 4. 2023 | Type Safety in 10 Easy, 4 Medium, and 1 Hard Lemma using Step-indexed Logical Relations – siek.blogspot.com
|
| 8. 4. 2022 | Using Agda's Induction/Recursion Library – siek.blogspot.com
|
| 28. 3. 2021 | Strongly Connected Components and Kosaraju's Algorithm – siek.blogspot.com
|
| 12. 7. 2020 | Type Safety in Two Easy Lemmas – siek.blogspot.com
|
| 12. 9. 2018 | Reading list for getting started on Gradual Typing – siek.blogspot.com
|
| 10. 8. 2018 | Intersection Types, Sub-formula Property, and the Functional Character of the Lambda Calculus – siek.blogspot.com
|
| 11. 5. 2018 | Type Safety in Three Easy Lemmas – siek.blogspot.com
|
| 29. 4. 2018 | What do real numbers have in common with lambdas? and what does continuity have to do with it? – siek.blogspot.com
|
| 24. 12. 2017 | Putting the Function back in Lambda – siek.blogspot.com
|
| 18. 10. 2017 | New revision of the semantics paper (POPL rejection, ESOP submission) – siek.blogspot.com
|
| 6. 10. 2017 | Comparing to Plotkin and Engeler's Set-theoretic Models of the Lambda Calculus – siek.blogspot.com
|
| 13. 7. 2017 | POPL submission, pulling together these blog posts on semantics! – siek.blogspot.com
|
| 8. 6. 2017 | Revisiting "well-typed programs cannot go wrong" – siek.blogspot.com
|
| 25. 3. 2017 | Consolidation of the Denotational Semantics and an Application to Compiler Correctness – siek.blogspot.com
|
| 11. 3. 2017 | The Take 3 Semantics, Revisited – siek.blogspot.com
|
| 11. 3. 2017 | Intersection Types as Denotations – siek.blogspot.com
|
| 9. 3. 2017 | Sound wrt. Contextual Equivalence – siek.blogspot.com
|
| 9. 3. 2017 | On the Meaning of Casts and Blame for Gradual Typing – siek.blogspot.com
|
| 1. 2. 2017 | Completeness of Intersection Types wrt. an Applied CBV Lambda Calculus – siek.blogspot.com
|
| 14. 1. 2017 | Simple Denotational Semantics for the Lambda Calculus, Pω Revisited? – siek.blogspot.com
|
| 7. 1. 2017 | Take 3: Application with Subsumption for Den. Semantics of Lambda Calculus – siek.blogspot.com
|
| 19. 12. 2016 | Take 2: Graph of Tables for the Denotational Semantics of the Lambda Calculus – siek.blogspot.com
|
| 16. 12. 2016 | Denotational Semantics of IMP without the Least Fixed Point – siek.blogspot.com
|
| 22. 4. 2014 | The Publication Process in Programming Languages – siek.blogspot.com
|
| 27. 10. 2012 | Is TypeScript gradually typed? Part 1 – siek.blogspot.com
|
| 21. 10. 2012 | Interp. of the GTLC, Part 5: Eager Cast Checking – siek.blogspot.com
|
| 9. 10. 2012 | Is TypeScript gradually typed? Part 2 – siek.blogspot.com
|
| 20. 9. 2012 | Interpretations of the GTLC, Part 4: Even Faster – siek.blogspot.com
|
| 20. 9. 2012 | Interpretations of the GTLC: Part 3, Going Faster – siek.blogspot.com |