corpus.blog
41554 blogs · [ { "id": "01a087cc-f4f1-7089-af86-618849c0234d", "title": "The alpha disaster", "url": "https://queuea9.wordpress.com/2026/08/18/the-alpha-disaster/", "published_at": "2026-08-18T18:00:56+00:00" }, { "id": "01a087cc-f4f1-7089-af86-61884a35f276", "title": "Slides on Measure-Based Termination for STLC", "url": "https://queuea9.wordpress.com/2025/11/17/slides-on-measure-based-termination-for-stlc/", "published_at": "2025-11-18T04:05:49+00:00" }, { "id": "01a087cc-f4f1-7089-af86-61884aed2e19", "title": "Notes for “The Stunner”", "url": "https://queuea9.wordpress.com/2025/08/19/notes-for-the-stunner/", "published_at": "2025-08-19T21:59:54+00:00" }, { "id": "01a087cc-f4f1-7089-af86-61884bb008f2", "title": "A Script for Wadler’s Parable of LEM", "url": "https://queuea9.wordpress.com/2025/04/30/a-script-for-wadlers-parable-of-lem/", "published_at": "2025-04-30T20:14:17+00:00" }, { "id": "01a087cc-f4f1-7089-af86-61884c3175a3", "title": "A Measure-Based Proof of the Finite Developments Theorem", "url": "https://queuea9.wordpress.com/2025/04/16/a-measure-based-proof-of-the-finite-developments-theorem/", "published_at": "2025-04-16T21:39:03+00:00" }, { "id": "01a087cc-f4f1-7089-af86-61884c84c357", "title": "Could tail be a fold?", "url": "https://queuea9.wordpress.com/2024/10/07/the-tail-function-is-a-fold/", "published_at": "2024-10-07T16:34:52+00:00" }, { "id": "01a087cc-f4f1-7089-af86-61884d8161a4", "title": "What kind of principle is parametricity?", "url": "https://queuea9.wordpress.com/2024/07/11/what-kind-of-principle-is-parametricity/", "published_at": "2024-07-12T03:55:00+00:00" }, { "id": "01a087cc-f4f1-7089-af86-61884dcc90ca", "title": "Logging, pure and simple", "url": "https://queuea9.wordpress.com/2023/12/28/logging-pure-and-simple/", "published_at": "2023-12-28T22:01:36+00:00" }, { "id": "01a087cc-f4f1-7089-af86-61884e29dce5", "title": "Practical Strong Functional Programming", "url": "https://queuea9.wordpress.com/2023/06/13/practical-strong-functional-programming/", "published_at": "2023-06-13T23:28:11+00:00" }, { "id": "01a087cc-f4f1-7089-af86-61884e5763b0", "title": "Predecessor with maybe", "url": "https://queuea9.wordpress.com/2022/12/06/predecessor-with-maybe/", "published_at": "2022-12-06T06:16:30+00:00" }, { "id": "01a0bdf1-1a25-707b-9019-2a9f738aae89", "title": "Deriving a case of the omega-rule in pure lambda calculus", "url": "https://queuea9.wordpress.com/2022/03/06/deriving-a-case-of-the-omega-rule-in-pure-lambda-calculus/", "published_at": "2022-03-07T04:47:10+00:00" }, { "id": "01a0bdf1-1a25-707b-9019-2a9f7445e7ff", "title": "And what, pray tell, is a universe?", "url": "https://queuea9.wordpress.com/2021/12/09/and-what-pray-tell-is-a-universe/", "published_at": "2021-12-10T05:07:35+00:00" }, { "id": "01a0bdf1-1a25-707b-9019-2a9f75019aa3", "title": "Care to Comment?", "url": "https://queuea9.wordpress.com/2021/08/17/care-to-comment/", "published_at": "2021-08-17T16:40:43+00:00" }, { "id": "01a0bdf1-1a25-707b-9019-2a9f7547f9f2", "title": "Another Optimality Challenge", "url": "https://queuea9.wordpress.com/2021/04/30/another-optimality-challenge/", "published_at": "2021-05-01T05:24:34+00:00" }, { "id": "01a0bdf1-1a25-707b-9019-2a9f763759da", "title": "Some thoughts on “Types, Abstraction, and Parametric Polymorphism”", "url": "https://queuea9.wordpress.com/2020/11/25/some-thoughts-on-types-abstraction-and-parametric-polymorphism/", "published_at": "2020-11-26T05:31:32+00:00" }, { "id": "01a0bdf1-1a25-707b-9019-2a9f77062b7f", "title": "And the winner is…", "url": "https://queuea9.wordpress.com/2020/07/12/and-the-winner-is/", "published_at": "2020-07-13T05:20:54+00:00" }, { "id": "01a0bdf1-1a25-707b-9019-2a9f77f68b2a", "title": "Show me the (optimal) beta [updated again]", "url": "https://queuea9.wordpress.com/2020/07/10/show-me-the-optimal-beta/", "published_at": "2020-07-11T04:32:22+00:00" }, { "id": "01a0bdf1-1a25-707b-9019-2a9f7845ac28", "title": "An intuition for reflection", "url": "https://queuea9.wordpress.com/2020/04/01/an-intuition-for-reflection/", "published_at": "2020-04-01T17:06:55+00:00" }, { "id": "01a0bdf1-1a25-707b-9019-2a9f7861c463", "title": "Announcing a podcast", "url": "https://queuea9.wordpress.com/2019/11/21/announcing-a-podcast/", "published_at": "2019-11-21T20:25:29+00:00" }, { "id": "01a0bdf1-1a25-707b-9019-2a9f78d1f0e3", "title": "What is a recursion universe? (and where can I get mine?)", "url": "https://queuea9.wordpress.com/2019/10/11/what-is-a-recursion-universe-and-where-can-i-get-mine/", "published_at": "2019-10-11T21:51:37+00:00" }, { "id": "01a0be02-bee1-7115-b58a-6c838c92c456", "title": "In Praise of Strong FP", "url": "https://queuea9.wordpress.com/2019/07/25/in-praise-of-strong-fp/", "published_at": "2019-07-25T19:09:51+00:00" }, { "id": "01a0be02-bee1-7115-b58a-6c838d55aa0e", "title": "Invited talk at LOLA ’19", "url": "https://queuea9.wordpress.com/2019/07/17/invited-talk-at-lola-19/", "published_at": "2019-07-17T21:18:24+00:00" }, { "id": "01a0be02-bee1-7115-b58a-6c838e11a21f", "title": "Guest column: Andrew Marmaduke’s report from DevCon4", "url": "https://queuea9.wordpress.com/2019/03/01/guest-column-andrew-marmadukes-report-from-devcon4/", "published_at": "2019-03-02T03:05:10+00:00" }, { "id": "01a0be02-bee1-7115-b58a-6c838e90a4ef", "title": "Guest column: Chris Jenkins’s report from IFL ’18", "url": "https://queuea9.wordpress.com/2019/03/01/guest-column-chris-jenkinss-report-from-ifl-18/", "published_at": "2019-03-02T03:00:01+00:00" }, { "id": "01a0be02-bee1-7115-b58a-6c838f702723", "title": "Why I no longer believe in computational classical type theory", "url": "https://queuea9.wordpress.com/2018/10/17/why-i-no-longer-believe-in-computational-classical-type-theory/", "published_at": "2018-10-18T05:48:43+00:00" }, { "id": "01a0be02-bee1-7115-b58a-6c838feda9e3", "title": "Cedille 1.0.0 coming Friday", "url": "https://queuea9.wordpress.com/2018/09/12/cedille-1-0-0-coming-friday/", "published_at": "2018-09-13T04:59:45+00:00" }, { "id": "01a0be02-bee1-7115-b58a-6c83906006e4", "title": "What is semantics?", "url": "https://queuea9.wordpress.com/2018/08/29/what-is-semantics/", "published_at": "2018-08-29T21:59:59+00:00" }, { "id": "01a0be02-bee1-7115-b58a-6c839116c535", "title": "FLOC 2018 Highlights (Guest Post)", "url": "https://queuea9.wordpress.com/2018/08/09/floc-2018-highlights/", "published_at": "2018-08-09T12:00:15+00:00" }, { "id": "01a0be02-bee1-7115-b58a-6c8391461e58", "title": "Optimal beta-reduction: lecture 2", "url": "https://queuea9.wordpress.com/2018/06/22/optimal-beta-reduction-lecture-2/", "published_at": "2018-06-22T18:46:09+00:00" }, { "id": "01a0be02-bee1-7115-b58a-6c839238f680", "title": "Optimal beta-reduction: lecture 1", "url": "https://queuea9.wordpress.com/2018/06/06/optimal-beta-reduction-lecture-1/", "published_at": "2018-06-06T19:00:35+00:00" }, { "id": "01a0be09-5b28-7010-975b-d926625fe4e2", "title": "State of Cedille", "url": "https://queuea9.wordpress.com/2017/09/02/state-of-cedille/", "published_at": "2017-09-03T02:11:17+00:00" }, { "id": "01a0be09-5b28-7010-975b-d9266350f848", "title": "Talk on Ethics and Technology", "url": "https://queuea9.wordpress.com/2017/05/06/talk-on-ethics-and-technology/", "published_at": "2017-05-07T03:36:38+00:00" }, { "id": "01a0be09-5b28-7010-975b-d92663ea0c73", "title": "Recursive types and fixed points", "url": "https://queuea9.wordpress.com/2017/04/20/recursive-types-and-fixed-points/", "published_at": "2017-04-20T21:16:24+00:00" }, { "id": "01a0be09-5b28-7010-975b-d92664ac6727", "title": "What do you do at the top of the ladder?", "url": "https://queuea9.wordpress.com/2017/03/15/what-do-you-do-at-the-top-of-the-ladder/", "published_at": "2017-03-15T18:50:13+00:00" }, { "id": "01a0be09-5b28-7010-975b-d926657ff4c4", "title": "Type Theory Podcast", "url": "https://queuea9.wordpress.com/2016/12/01/type-theory-podcast/", "published_at": "2016-12-02T04:57:40+00:00" }, { "id": "01a0be09-5b28-7010-975b-d92665f1bd13", "title": "News You Can’t Use", "url": "https://queuea9.wordpress.com/2016/11/12/news-you-cant-use/", "published_at": "2016-11-13T03:57:05+00:00" }, { "id": "01a0be09-5b28-7010-975b-d92666923b90", "title": "Well-founded recursion considered harmful", "url": "https://queuea9.wordpress.com/2016/08/15/well-founded-recursion-considered-harmful/", "published_at": "2016-08-15T20:03:12+00:00" }, { "id": "01a0be09-5b28-7010-975b-d92666da3b3d", "title": "The Impredicativity of Induction", "url": "https://queuea9.wordpress.com/2016/03/04/the-impredicativity-of-induction/", "published_at": "2016-03-05T03:27:38+00:00" }, { "id": "01a0be09-5b28-7010-975b-d9266772b54b", "title": "From Logic with Love", "url": "https://queuea9.wordpress.com/2015/12/01/from-logic-with-love/", "published_at": "2015-12-01T21:51:17+00:00" }, { "id": "01a0be09-5b28-7010-975b-d926677c6be1", "title": "Craig’s Theorem", "url": "https://queuea9.wordpress.com/2015/11/11/craigs-theorem/", "published_at": "2015-11-11T21:41:57+00:00" } ] posts Claim your blog
Back to queuea9.wordpress.com
Blog · corpus.blog/blogs/queuea9.wordpress.com/posts

queuea9.wordpress.com

queuea9.wordpress.com

2026

The alpha disasteroriginal ↗
18 Aug 2026

2025

Slides on Measure-Based Termination for STLCoriginal ↗
18 Nov 2025
Notes for “The Stunner”original ↗
19 Aug 2025
A Script for Wadler’s Parable of LEMoriginal ↗
30 Apr 2025
A Measure-Based Proof of the Finite Developments Theoremoriginal ↗
16 Apr 2025

2024

Could tail be a fold?original ↗
7 Oct 2024
What kind of principle is parametricity?original ↗
12 Jul 2024

2023

Logging, pure and simpleoriginal ↗
28 Dec 2023
Practical Strong Functional Programmingoriginal ↗
13 Jun 2023

2022

Predecessor with maybeoriginal ↗
6 Dec 2022
Deriving a case of the omega-rule in pure lambda calculusoriginal ↗
7 Mar 2022

2021

And what, pray tell, is a universe?original ↗
10 Dec 2021
Care to Comment?original ↗
17 Aug 2021
Another Optimality Challengeoriginal ↗
1 May 2021

2020

Some thoughts on “Types, Abstraction, and Parametric Polymorphism”original ↗
26 Nov 2020
And the winner is…original ↗
13 Jul 2020
Show me the (optimal) beta [updated again]original ↗
11 Jul 2020
An intuition for reflectionoriginal ↗
1 Apr 2020

2019

Announcing a podcastoriginal ↗
21 Nov 2019
What is a recursion universe? (and where can I get mine?)original ↗
11 Oct 2019
In Praise of Strong FPoriginal ↗
25 Jul 2019
Invited talk at LOLA ’19original ↗
17 Jul 2019
Guest column: Andrew Marmaduke’s report from DevCon4original ↗
2 Mar 2019
Guest column: Chris Jenkins’s report from IFL ’18original ↗
2 Mar 2019

2018

Why I no longer believe in computational classical type theoryoriginal ↗
18 Oct 2018
Cedille 1.0.0 coming Fridayoriginal ↗
13 Sept 2018
What is semantics?original ↗
29 Aug 2018
FLOC 2018 Highlights (Guest Post)original ↗
9 Aug 2018
Optimal beta-reduction: lecture 2original ↗
22 Jun 2018
Optimal beta-reduction: lecture 1original ↗
6 Jun 2018

2017

State of Cedilleoriginal ↗
3 Sept 2017
Talk on Ethics and Technologyoriginal ↗
7 May 2017
Recursive types and fixed pointsoriginal ↗
20 Apr 2017
What do you do at the top of the ladder?original ↗
15 Mar 2017

2016

Type Theory Podcastoriginal ↗
2 Dec 2016
News You Can’t Useoriginal ↗
13 Nov 2016
Well-founded recursion considered harmfuloriginal ↗
15 Aug 2016
The Impredicativity of Inductionoriginal ↗
5 Mar 2016

2015

From Logic with Loveoriginal ↗
1 Dec 2015
Craig’s Theoremoriginal ↗
11 Nov 2015