corpus.blog
41554 blogs · [ { "id": "01a087e0-880c-72bc-9fd2-f7de95d56cf1", "title": "Take-aways from using Deduce in the classroom", "url": "https://siek.blogspot.com/2024/10/take-aways-from-using-deduce-in.html", "published_at": "2024-10-09T20:58:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de96aee41a", "title": "Binary Search Trees, Correctly!", "url": "https://siek.blogspot.com/2024/08/binary-search-trees-correctly.html", "published_at": "2024-08-11T19:04:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de96ea1e1f", "title": "Binary Trees with In-order Iterators (Part 2)", "url": "https://siek.blogspot.com/2024/07/binary-trees-with-in-order-iterators_20.html", "published_at": "2024-07-20T20:57:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de977743bb", "title": "Binary Trees with In-order Iterators (Part 1)", "url": "https://siek.blogspot.com/2024/07/binary-trees-with-in-order-iterators.html", "published_at": "2024-07-18T19:28:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9838d80c", "title": "Merge Sort with Leftovers, Correctly", "url": "https://siek.blogspot.com/2024/06/merge-sort-with-leftovers-correctly.html", "published_at": "2024-06-30T14:45:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9858f3c7", "title": "Insertion Sort, Correctly", "url": "https://siek.blogspot.com/2024/06/insertion-sort-correctly.html", "published_at": "2024-06-17T17:29:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de98fe52e5", "title": "Sequential Search, Correctly", "url": "https://siek.blogspot.com/2024/06/sequential-search-correctly.html", "published_at": "2024-06-14T20:20:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9976fa5d", "title": "Data Structures and Algorithms, Correctly", "url": "https://siek.blogspot.com/2024/06/data-structures-and-algorithms-correctly.html", "published_at": "2024-06-12T15:44:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de99de40cc", "title": "Help! We're Failing to Prove Correctness of Closure Conversion using Denotational Semantics (Graph Models)", "url": "https://siek.blogspot.com/2023/06/help-were-failing-to-prove-correctness.html", "published_at": "2023-06-08T15:25:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9a5dc087", "title": "Gradual Guarantee via Step-indexed Logical Relations", "url": "https://siek.blogspot.com/2023/05/gradual-guarantee-via-step-indexed.html", "published_at": "2023-05-16T23:28:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9ac161be", "title": "Type Safety in 10 Easy, 4 Medium, and 1 Hard Lemma using Step-indexed Logical Relations", "url": "https://siek.blogspot.com/2023/04/type-safety-in-10-easy-4-medium-and-1.html", "published_at": "2023-04-17T16:15:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9af0778a", "title": "Using Agda's Induction/Recursion Library", "url": "https://siek.blogspot.com/2022/04/using-agdas-inductionrecursion-library.html", "published_at": "2022-04-07T14:56:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9b7407bc", "title": "Strongly Connected Components and Kosaraju's Algorithm", "url": "https://siek.blogspot.com/2021/03/strongly-connected-components-and.html", "published_at": "2021-03-27T20:43:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9b8b8d7b", "title": "Type Safety in Two Easy Lemmas", "url": "https://siek.blogspot.com/2020/07/type-safety-in-two-easy-lemmas.html", "published_at": "2020-07-10T20:11:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9bbfc0dd", "title": "Reading list for getting started on Gradual Typing", "url": "https://siek.blogspot.com/2018/09/reading-list-for-getting-started-on.html", "published_at": "2018-09-12T12:51:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9c57bd7e", "title": "Intersection Types, Sub-formula Property, and the Functional Character of the Lambda Calculus", "url": "https://siek.blogspot.com/2018/08/intersection-types-sub-formula-property.html", "published_at": "2018-08-09T14:32:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9c9e1d3b", "title": "What do real numbers have in common with lambdas? and what does continuity have to do with it?", "url": "https://siek.blogspot.com/2018/04/what-do-real-numbers-have-in-common.html", "published_at": "2018-04-25T03:31:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9d941411", "title": "Putting the Function back in Lambda", "url": "https://siek.blogspot.com/2017/12/putting-function-back-in-lambda.html", "published_at": "2017-12-24T04:04:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9e709174", "title": "New revision of the semantics paper (POPL rejection, ESOP submission)", "url": "https://siek.blogspot.com/2017/10/new-revision-of-semantics-paper-popl.html", "published_at": "2017-10-15T21:54:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9e98533f", "title": "Comparing to Plotkin and Engeler's Set-theoretic Models of the Lambda Calculus", "url": "https://siek.blogspot.com/2017/10/comparing-to-plotkin-and-engelers-set.html", "published_at": "2017-10-04T00:43:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9edc883c", "title": "POPL submission, pulling together these blog posts on semantics!", "url": "https://siek.blogspot.com/2017/07/popl-submission-pulling-together-these.html", "published_at": "2017-07-13T15:44:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7de9fd3429e", "title": "Revisiting \"well-typed programs cannot go wrong\"", "url": "https://siek.blogspot.com/2017/06/revisiting-well-typed-programs-cannot.html", "published_at": "2017-06-08T04:04:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7dea0a16f4a", "title": "Consolidation of the Denotational Semantics and an Application to Compiler Correctness", "url": "https://siek.blogspot.com/2017/03/consolidation-of-denotational-semantics.html", "published_at": "2017-03-24T18:20:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7dea0bfda34", "title": "The Take 3 Semantics, Revisited", "url": "https://siek.blogspot.com/2017/03/the-take-3-semantics-revisited.html", "published_at": "2017-03-11T04:31:00+00:00" }, { "id": "01a087e0-880c-72bc-9fd2-f7dea12a92e1", "title": "Sound wrt. Contextual Equivalence", "url": "https://siek.blogspot.com/2017/03/sound-wrt-contextual-equivalence.html", "published_at": "2017-03-08T16:59:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d0e6e10f6", "title": "On the Meaning of Casts and Blame for Gradual Typing", "url": "https://siek.blogspot.com/2017/02/on-meaning-of-casts-and-blame-for.html", "published_at": "2017-02-05T20:39:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d0eebadbf", "title": "Completeness of Intersection Types wrt. an Applied CBV Lambda Calculus", "url": "https://siek.blogspot.com/2017/01/completeness-of-intersection-types-wrt.html", "published_at": "2017-01-31T04:33:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d0fbe7444", "title": "Intersection Types as Denotations", "url": "https://siek.blogspot.com/2017/01/intersection-types-as-denotations.html", "published_at": "2017-01-14T23:40:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d107c5b4d", "title": "Take 3: Application with Subsumption for Den. Semantics of Lambda Calculus", "url": "https://siek.blogspot.com/2016/12/take-3-application-with-subsumption-for.html", "published_at": "2016-12-21T21:48:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d1169d5bd", "title": "Take 2: Graph of Tables for the Denotational Semantics of the Lambda Calculus", "url": "https://siek.blogspot.com/2016/12/take-2-graph-of-tables-for-denotational.html", "published_at": "2016-12-19T12:57:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d1222abee", "title": "Simple Denotational Semantics for the Lambda Calculus, Pω Revisited?", "url": "https://siek.blogspot.com/2016/12/simple-denotational-semantics-for.html", "published_at": "2016-12-16T05:56:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d128ef6f0", "title": "Denotational Semantics of IMP without the Least Fixed Point", "url": "https://siek.blogspot.com/2016/12/denotational-semantics-of-imp-without.html", "published_at": "2016-12-09T03:55:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d12c9a17e", "title": "The Publication Process in Programming Languages", "url": "https://siek.blogspot.com/2014/01/the-publication-process-in-programming.html", "published_at": "2014-01-27T04:10:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d13c91a9f", "title": "Type Safety in Three Easy Lemmas", "url": "https://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html", "published_at": "2013-05-27T12:52:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d145fd721", "title": "Interp. of the GTLC, Part 5: Eager Cast Checking", "url": "https://siek.blogspot.com/2012/10/interp-of-gtlc-part-5-eager-cast.html", "published_at": "2012-10-19T04:50:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d14ca870d", "title": "Is TypeScript gradually typed? Part 2", "url": "https://siek.blogspot.com/2012/10/is-typescript-gradually-typed-part-2.html", "published_at": "2012-10-09T05:25:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d15b3b87e", "title": "Is TypeScript gradually typed? Part 1", "url": "https://siek.blogspot.com/2012/10/is-typescript-gradually-typed-part-1.html", "published_at": "2012-10-04T17:25:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d168a8f0a", "title": "Interpretations of the GTLC, Part 4: Even Faster", "url": "https://siek.blogspot.com/2012/09/interpretations-of-gtlc-part-4-even.html", "published_at": "2012-09-20T17:53:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d1712899f", "title": "Interpretations of the GTLC: Part 3, Going Faster", "url": "https://siek.blogspot.com/2012/09/interpretations-of-gtlc-part-3-going.html", "published_at": "2012-09-19T22:40:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d180c5cdf", "title": "Interpretations of the GTLC, Part 2: Space-Efficient Machines", "url": "https://siek.blogspot.com/2012/09/interpretations-of-gtlc-part-2.html", "published_at": "2012-09-18T18:48:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d18e93d1d", "title": "Interpretations of the Gradually-Typed Lambda Calculus, Part 1", "url": "https://siek.blogspot.com/2012/09/interpretations-of-gradually-typed.html", "published_at": "2012-09-18T04:55:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d197bcc0e", "title": "Rationale for \"Type Safety in Five\"", "url": "https://siek.blogspot.com/2012/08/rationale-for-type-safety-in-five.html", "published_at": "2012-08-29T17:27:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d1a5b44f5", "title": "Type Safety in Five Easy Lemmas", "url": "https://siek.blogspot.com/2012/08/type-safety-in-five-easy-lemmas.html", "published_at": "2012-08-24T23:08:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d1ae0997a", "title": "The Work Horse of PL Theory: Structural Induction", "url": "https://siek.blogspot.com/2012/08/structural-induction-work-horse-of-pl.html", "published_at": "2012-08-13T18:15:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d1b230f1e", "title": "Compositional Separate Compilation, Take Three", "url": "https://siek.blogspot.com/2012/08/compositional-separate-compilation-take.html", "published_at": "2012-08-10T20:14:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d1bbfd0f2", "title": "How to Prove It", "url": "https://siek.blogspot.com/2012/08/how-to-prove-it.html", "published_at": "2012-08-07T17:58:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d1c4f5524", "title": "Separate Compilation, Take Two, Compositionally", "url": "https://siek.blogspot.com/2012/08/separate-compilation-take-two.html", "published_at": "2012-08-06T05:20:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d1c50fdf5", "title": "Historical note: Algol 60 was an early metaprogramming lang.", "url": "https://siek.blogspot.com/2012/08/historical-note-algol-60-was-early.html", "published_at": "2012-08-05T14:45:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d1cd9104b", "title": "The Semantics of a Familiar Language: Featherweight C", "url": "https://siek.blogspot.com/2012/07/the-semantics-of-familiar-language.html", "published_at": "2012-07-30T19:48:00+00:00" }, { "id": "01a0cf76-b894-70ef-b0f4-444d1db4901b", "title": "Crash Course on Notation in Programming Language Theory", "url": "https://siek.blogspot.com/2012/07/crash-course-on-notation-in-programming.html", "published_at": "2012-07-26T19:27:00+00:00" }, { "id": "01a0cf77-1002-73e2-aaa7-c84512428030", "title": "Big-step, diverging or stuck?", "url": "https://siek.blogspot.com/2012/07/big-step-diverging-or-stuck.html", "published_at": "2012-07-25T19:59:00+00:00" }, { "id": "01a0cf77-1002-73e2-aaa7-c8451319adb5", "title": "Linking isn't substitution: the separately-compiled lambda calculus", "url": "https://siek.blogspot.com/2012/07/linking-isnt-substitution-separately.html", "published_at": "2012-07-18T06:29:00+00:00" }, { "id": "01a0cf77-1002-73e2-aaa7-c8451371ffb5", "title": "Over-specification in operational semantics, or the case of the missing \"eval\"", "url": "https://siek.blogspot.com/2012/07/over-specification-in-operational.html", "published_at": "2012-07-16T00:14:00+00:00" }, { "id": "01a0cf77-1002-73e2-aaa7-c84513a3c4c9", "title": "My new favorite abstract machine: ECD on ANF", "url": "https://siek.blogspot.com/2012/07/my-new-favorite-abstract-machine-ecd-on.html", "published_at": "2012-07-12T20:41:00+00:00" }, { "id": "01a0cf77-1002-73e2-aaa7-c8451462b526", "title": "Closure Conversion, with Polymorphism", "url": "https://siek.blogspot.com/2012/07/closure-conversion-with-polymorphism.html", "published_at": "2012-07-10T05:00:00+00:00" }, { "id": "01a0cf77-1002-73e2-aaa7-c845150c5c45", "title": "The Essence of Closure Conversion", "url": "https://siek.blogspot.com/2012/07/essence-of-closure-conversion.html", "published_at": "2012-07-08T06:14:00+00:00" }, { "id": "01a0cf77-1002-73e2-aaa7-c8451539e938", "title": "First-class Cases", "url": "https://siek.blogspot.com/2012/06/first-class-cases.html", "published_at": "2012-06-29T20:55:00+00:00" }, { "id": "01a0cf77-1002-73e2-aaa7-c845153eba03", "title": "The ECD Abstract Machine, A Programmer's Operational Semantics", "url": "https://siek.blogspot.com/2009/12/ecd-abstract-machine-programmers.html", "published_at": "2009-12-21T23:49:00+00:00" }, { "id": "01a0cf77-1002-73e2-aaa7-c84516216681", "title": "Greatest Common Divisor", "url": "https://siek.blogspot.com/2009/12/greatest-common-divisor.html", "published_at": "2009-12-05T06:41:00+00:00" }, { "id": "01a0cf77-1002-73e2-aaa7-c8451717c09a", "title": "Strong Induction", "url": "https://siek.blogspot.com/2009/11/strong-induction.html", "published_at": "2009-11-30T09:12:00+00:00" } ] posts Claim your blog
Back to siek.blogspot.com
Blog · corpus.blog/blogs/siek.blogspot.com/posts

siek.blogspot.com

siek.blogspot.com

2024

Take-aways from using Deduce in the classroomoriginal ↗
9 Oct 2024
Binary Search Trees, Correctly!original ↗
11 Aug 2024
Binary Trees with In-order Iterators (Part 2)original ↗
20 Jul 2024
Binary Trees with In-order Iterators (Part 1)original ↗
18 Jul 2024
Merge Sort with Leftovers, Correctlyoriginal ↗
30 Jun 2024
Insertion Sort, Correctlyoriginal ↗
17 Jun 2024
Sequential Search, Correctlyoriginal ↗
14 Jun 2024
Data Structures and Algorithms, Correctlyoriginal ↗
12 Jun 2024

2023

Help! We're Failing to Prove Correctness of Closure Conversion using Denotational Semantics (Graph Models)original ↗
8 Jun 2023
Gradual Guarantee via Step-indexed Logical Relationsoriginal ↗
16 May 2023
Type Safety in 10 Easy, 4 Medium, and 1 Hard Lemma using Step-indexed Logical Relationsoriginal ↗
17 Apr 2023

2022

Using Agda's Induction/Recursion Libraryoriginal ↗
7 Apr 2022

2021

Strongly Connected Components and Kosaraju's Algorithmoriginal ↗
27 Mar 2021

2020

Type Safety in Two Easy Lemmasoriginal ↗
10 Jul 2020

2018

Reading list for getting started on Gradual Typingoriginal ↗
12 Sept 2018
Intersection Types, Sub-formula Property, and the Functional Character of the Lambda Calculusoriginal ↗
9 Aug 2018
What do real numbers have in common with lambdas? and what does continuity have to do with it?original ↗
25 Apr 2018

2017

Putting the Function back in Lambdaoriginal ↗
24 Dec 2017
New revision of the semantics paper (POPL rejection, ESOP submission)original ↗
15 Oct 2017
Comparing to Plotkin and Engeler's Set-theoretic Models of the Lambda Calculusoriginal ↗
4 Oct 2017
POPL submission, pulling together these blog posts on semantics!original ↗
13 Jul 2017
Revisiting "well-typed programs cannot go wrong"original ↗
8 Jun 2017
Consolidation of the Denotational Semantics and an Application to Compiler Correctnessoriginal ↗
24 Mar 2017
The Take 3 Semantics, Revisitedoriginal ↗
11 Mar 2017
Sound wrt. Contextual Equivalenceoriginal ↗
8 Mar 2017
On the Meaning of Casts and Blame for Gradual Typingoriginal ↗
5 Feb 2017
Completeness of Intersection Types wrt. an Applied CBV Lambda Calculusoriginal ↗
31 Jan 2017
Intersection Types as Denotationsoriginal ↗
14 Jan 2017

2016

Take 3: Application with Subsumption for Den. Semantics of Lambda Calculusoriginal ↗
21 Dec 2016
Take 2: Graph of Tables for the Denotational Semantics of the Lambda Calculusoriginal ↗
19 Dec 2016
Simple Denotational Semantics for the Lambda Calculus, Pω Revisited?original ↗
16 Dec 2016
Denotational Semantics of IMP without the Least Fixed Pointoriginal ↗
9 Dec 2016

2014

The Publication Process in Programming Languagesoriginal ↗
27 Jan 2014

2013

Type Safety in Three Easy Lemmasoriginal ↗
27 May 2013

2012

Interp. of the GTLC, Part 5: Eager Cast Checkingoriginal ↗
19 Oct 2012
Is TypeScript gradually typed? Part 2original ↗
9 Oct 2012
Is TypeScript gradually typed? Part 1original ↗
4 Oct 2012
Interpretations of the GTLC, Part 4: Even Fasteroriginal ↗
20 Sept 2012
Interpretations of the GTLC: Part 3, Going Fasteroriginal ↗
19 Sept 2012
Interpretations of the GTLC, Part 2: Space-Efficient Machinesoriginal ↗
18 Sept 2012
Interpretations of the Gradually-Typed Lambda Calculus, Part 1original ↗
18 Sept 2012
Rationale for "Type Safety in Five"original ↗
29 Aug 2012
Type Safety in Five Easy Lemmasoriginal ↗
24 Aug 2012
The Work Horse of PL Theory: Structural Inductionoriginal ↗
13 Aug 2012
Compositional Separate Compilation, Take Threeoriginal ↗
10 Aug 2012
How to Prove Itoriginal ↗
7 Aug 2012
Separate Compilation, Take Two, Compositionallyoriginal ↗
6 Aug 2012
Historical note: Algol 60 was an early metaprogramming lang.original ↗
5 Aug 2012
The Semantics of a Familiar Language: Featherweight Coriginal ↗
30 Jul 2012
Crash Course on Notation in Programming Language Theoryoriginal ↗
26 Jul 2012
Big-step, diverging or stuck?original ↗
25 Jul 2012
Linking isn't substitution: the separately-compiled lambda calculusoriginal ↗
18 Jul 2012
Over-specification in operational semantics, or the case of the missing "eval"original ↗
16 Jul 2012
My new favorite abstract machine: ECD on ANForiginal ↗
12 Jul 2012
Closure Conversion, with Polymorphismoriginal ↗
10 Jul 2012
The Essence of Closure Conversionoriginal ↗
8 Jul 2012
First-class Casesoriginal ↗
29 Jun 2012

2009

The ECD Abstract Machine, A Programmer's Operational Semanticsoriginal ↗
21 Dec 2009
Greatest Common Divisororiginal ↗
5 Dec 2009
Strong Inductionoriginal ↗
30 Nov 2009