41554 blogs · [ { "id": "01a0dd0c-09e9-720e-bac6-b9bd985bc201", "title": "The Queen’s Gambit", "url": "https://refl.blog/2021/09/30/the-queens-gambit/", "published_at": "2021-09-30T09:12:28+00:00" }, { "id": "01a0dd0c-09e9-720e-bac6-b9bd98abc51d", "title": "Thinking, Fast & Slow Summary", "url": "https://refl.blog/2021/09/22/thinking-fast-slow-summary/", "published_at": "2021-09-22T17:36:44+00:00" }, { "id": "01a0dd0c-09e9-720e-bac6-b9bd98b42c27", "title": "Closed-expression of a sum with proof in Coq", "url": "https://refl.blog/2021/09/20/closed-expression-of-a-sum-with-proof-in-coq/", "published_at": "2021-09-20T11:34:16+00:00" }, { "id": "01a0dd0c-09e9-720e-bac6-b9bd9956fc5d", "title": "Bobby Fischer Teaches Chess Summary", "url": "https://refl.blog/2021/09/12/review-bobby-fischer-teaches-chess/", "published_at": "2021-09-12T09:42:04+00:00" }, { "id": "01a0dd0c-09e9-720e-bac6-b9bd99e180d1", "title": "Reflections on anxiety", "url": "https://refl.blog/2021/08/07/reflections-on-anxiety/", "published_at": "2021-08-07T20:17:46+00:00" }, { "id": "01a0dd0c-09e9-720e-bac6-b9bd9a57f304", "title": "Re-inventing the Monad wheel", "url": "https://refl.blog/2021/06/07/re-inventing-the-monad-wheel/", "published_at": "2021-06-07T06:16:27+00:00" }, { "id": "01a0dd0c-09e9-720e-bac6-b9bd9ae5a6b2", "title": "Algorithmic puzzle: Continuous Increasing Subsequences", "url": "https://refl.blog/2021/04/09/algorithmic-puzzle-continuous-increasing-subsequences/", "published_at": "2021-04-09T11:34:45+00:00" }, { "id": "01a0dd0c-09e9-720e-bac6-b9bd9b1e849b", "title": "Capturing Number Theory in Haskell", "url": "https://refl.blog/2021/04/05/capturing-number-theory-in-haskell/", "published_at": "2021-04-05T15:16:44+00:00" }, { "id": "01a0dd0c-09e9-720e-bac6-b9bd9b3afaad", "title": "Performant implementation of pagination on Cartesian products", "url": "https://refl.blog/2021/03/30/performant-implementation-of-pagination-on-cartesian-products/", "published_at": "2021-03-30T09:38:08+00:00" }, { "id": "01a0dd0c-09e9-720e-bac6-b9bd9be66cb6", "title": "Towards Hoare logic for a small imperative language in Haskell", "url": "https://refl.blog/2021/01/18/towards-hoare-logic-for-a-small-imperative-language-in-haskell/", "published_at": "2021-01-18T14:00:02+00:00" }, { "id": "01a0dd16-d324-724b-a269-c5168b8109ec", "title": "Reflecting on my FTH rotation", "url": "https://refl.blog/2021/01/15/reflecting-on-my-fth-rotation/", "published_at": "2021-01-15T10:46:00+00:00" }, { "id": "01a0dd16-d325-72af-afb9-ed79f63ebda3", "title": "Advent of Code #13", "url": "https://refl.blog/2020/12/24/advent-of-code-13/", "published_at": "2020-12-24T10:03:00+00:00" }, { "id": "01a0dd16-d325-72af-afb9-ed79f64fbe8b", "title": "Haskell memoization and evaluation model", "url": "https://refl.blog/2020/12/11/haskell-memoization-and-evaluation-model/", "published_at": "2020-12-11T14:02:32+00:00" }, { "id": "01a0dd16-d325-72af-afb9-ed79f6d8fb24", "title": "Advent of Code #8", "url": "https://refl.blog/2020/12/10/advent-of-code-8/", "published_at": "2020-12-10T20:17:31+00:00" }, { "id": "01a0dd16-d325-72af-afb9-ed79f75d59d0", "title": "Diversity and Bias", "url": "https://refl.blog/2020/10/22/diversity-and-bias/", "published_at": "2020-10-22T18:27:24+00:00" }, { "id": "01a0dd16-d325-72af-afb9-ed79f84e3c56", "title": "Proof: One Sunday every 7 days", "url": "https://refl.blog/2020/10/17/proof-one-sunday-every-7-days/", "published_at": "2020-10-17T17:01:21+00:00" }, { "id": "01a0dd16-d325-72af-afb9-ed79f9456d6c", "title": "On faith, unbelief, and doubt", "url": "https://refl.blog/2020/09/09/on-faith-unbelief-and-doubt/", "published_at": "2020-09-09T11:29:13+00:00" }, { "id": "01a0dd16-d325-72af-afb9-ed79f9d4bbce", "title": "Tenses", "url": "https://refl.blog/2020/09/03/tenses/", "published_at": "2020-09-03T11:08:54+00:00" }, { "id": "01a0dd16-d325-72af-afb9-ed79fa2879db", "title": "A simple Constraint Programming implementation", "url": "https://refl.blog/2020/08/22/a-simple-constraint-programming-implementation/", "published_at": "2020-08-22T11:24:25+00:00" }, { "id": "01a0dd16-d325-72af-afb9-ed79fa60dd31", "title": "Superliminal game overview", "url": "https://refl.blog/2020/08/21/superliminal-game-overview/", "published_at": "2020-08-21T10:08:03+00:00" }, { "id": "01a0dd25-969b-7342-9e5a-7a282885eb30", "title": "Proofs and computation with trees", "url": "https://refl.blog/2020/06/20/proofs-and-computation-with-trees/", "published_at": "2020-06-20T12:12:36+00:00" }, { "id": "01a0dd25-969b-7342-9e5a-7a2828cf3612", "title": "Deriving a Quine in a Lisp", "url": "https://refl.blog/2020/04/24/deriving-a-quine-in-a-lisp/", "published_at": "2020-04-24T16:49:17+00:00" }, { "id": "01a0dd25-969b-7342-9e5a-7a2829aa4416", "title": "Equational reasoning in Racket", "url": "https://refl.blog/2020/04/10/equational-reasoning-in-racket/", "published_at": "2020-04-10T16:39:07+00:00" }, { "id": "01a0dd25-969b-7342-9e5a-7a282a2e162f", "title": "Encoding probability and random variables in Racket", "url": "https://refl.blog/2020/04/05/encoding-probability-and-random-variables-in-racket/", "published_at": "2020-04-05T17:40:06+00:00" }, { "id": "01a0dd25-969b-7342-9e5a-7a282aced5e1", "title": "Stay Home", "url": "https://refl.blog/2020/03/14/stay-home/", "published_at": "2020-03-14T14:52:37+00:00" }, { "id": "01a0dd25-969b-7342-9e5a-7a282b7835a4", "title": "Formalization of Boolean algebra pt. 2", "url": "https://refl.blog/2020/02/01/formalization-of-boolean-algebra-pt-2/", "published_at": "2020-02-01T16:10:06+00:00" }, { "id": "01a0dd25-969b-7342-9e5a-7a282babb21b", "title": "Introduction and formalization of Boolean algebra", "url": "https://refl.blog/2020/01/31/introduction-and-formalization-of-boolean-algebra/", "published_at": "2020-01-31T17:16:43+00:00" }, { "id": "01a0dd25-969b-7342-9e5a-7a282c544c68", "title": "Wisdom of the crowd exercise", "url": "https://refl.blog/2020/01/25/wisdom-of-the-crowd-exercise/", "published_at": "2020-01-25T15:01:45+00:00" }, { "id": "01a0dd25-969b-7342-9e5a-7a282d4b75ce", "title": "Dafny proof to the Container With Most Water Problem", "url": "https://refl.blog/2020/01/05/dafny-proof-to-the-container-with-most-water-problem/", "published_at": "2020-01-05T20:21:44+00:00" }, { "id": "01a0dd25-969b-7342-9e5a-7a282e1ec741", "title": "GEB: An EGB overview (Part I)", "url": "https://refl.blog/2019/12/30/geb-an-egb-overview-part-i/", "published_at": "2019-12-30T16:30:34+00:00" }, { "id": "01a0dd35-6ad4-70e9-a602-aab434421835", "title": "Infinite power towers", "url": "https://refl.blog/2019/12/10/infinite-power-towers/", "published_at": "2019-12-10T11:17:18+00:00" }, { "id": "01a0dd35-6ad4-70e9-a602-aab435148a07", "title": "Idea: news diversity", "url": "https://refl.blog/2019/11/18/idea-news-diversity/", "published_at": "2019-11-18T11:08:57+00:00" }, { "id": "01a0dd35-6ad4-70e9-a602-aab4359f12af", "title": "Formalizing expressiveness of line editors", "url": "https://refl.blog/2019/11/09/formalizing-expresiveness-of-line-editors/", "published_at": "2019-11-09T17:48:47+00:00" }, { "id": "01a0dd35-6ad4-70e9-a602-aab435bc1a20", "title": "Proving Groups with Idris", "url": "https://refl.blog/2019/11/06/proving-groupoids-with-idris/", "published_at": "2019-11-06T13:06:15+00:00" }, { "id": "01a0dd35-6ad4-70e9-a602-aab4365a2bd3", "title": "A8c team meetup Athens, 2019", "url": "https://refl.blog/2019/11/04/a8c-team-meetup-athens-2019/", "published_at": "2019-11-04T13:02:50+00:00" }, { "id": "01a0dd35-6ad4-70e9-a602-aab436d46278", "title": "Metapost: Tuply singleton – Freedom of creativity", "url": "https://refl.blog/2019/10/19/metapost-tuply-singleton-freedom-of-creativity/", "published_at": "2019-10-19T11:11:23+00:00" }, { "id": "01a0dd35-6ad4-70e9-a602-aab4377953ab", "title": "Tuply singleton v3 (with proof)", "url": "https://refl.blog/2019/10/11/tuply-singleton-v3-with-proof/", "published_at": "2019-10-11T18:29:17+00:00" }, { "id": "01a0dd35-6ad4-70e9-a602-aab4386d9e15", "title": "Tuply singleton v2", "url": "https://refl.blog/2019/10/09/tuply-singleton-v2/", "published_at": "2019-10-09T13:48:22+00:00" }, { "id": "01a0dd35-6ad4-70e9-a602-aab438db113a", "title": "Tuply singleton", "url": "https://refl.blog/2019/10/06/tuply-singleton/", "published_at": "2019-10-06T18:12:20+00:00" }, { "id": "01a0dd35-6ad4-70e9-a602-aab439a93798", "title": "One plus one equals two", "url": "https://refl.blog/2019/09/20/one-plus-one-equals-two/", "published_at": "2019-09-20T09:47:34+00:00" }, { "id": "01a0dd50-e882-7168-8bdc-3863e88c47bd", "title": "Meet them all", "url": "https://refl.blog/2019/09/15/meet-them-all/", "published_at": "2019-09-15T11:10:04+00:00" }, { "id": "01a0dd50-e882-7168-8bdc-3863e9734433", "title": "Abstraction and generalization of objects", "url": "https://refl.blog/2019/08/08/abstraction-and-generalization-of-objects/", "published_at": "2019-08-08T12:10:42+00:00" }, { "id": "01a0dd50-e882-7168-8bdc-3863e9bb4283", "title": "Generalized average", "url": "https://refl.blog/2019/08/05/generalized-average/", "published_at": "2019-08-05T22:58:56+00:00" }, { "id": "01a0dd50-e882-7168-8bdc-3863eaa59e25", "title": "Arithmetic on Algebraic Data Types", "url": "https://refl.blog/2019/07/30/arithmetic-on-algebraic-data-types/", "published_at": "2019-07-30T16:09:41+00:00" }, { "id": "01a0dd50-e882-7168-8bdc-3863eb13dfe3", "title": "Brief introduction to Machine Learning with Gradient Descent", "url": "https://refl.blog/2019/07/10/brief-introduction-to-machine-learning-with-gradient-descent/", "published_at": "2019-07-10T21:42:02+00:00" }, { "id": "01a0dd50-e883-711e-8a10-99414f20545f", "title": "Naive Set Theory summary", "url": "https://refl.blog/2019/06/25/naive-set-theory-summary/", "published_at": "2019-06-25T12:57:58+00:00" }, { "id": "01a0dd50-e883-711e-8a10-99414f2fdfb1", "title": "Customer-driven engineering", "url": "https://refl.blog/2019/06/10/customer-driven-engineering/", "published_at": "2019-06-10T08:44:48+00:00" }, { "id": "01a0dd50-e883-711e-8a10-99414f9eb375", "title": "Lambda calculus with generalized abstraction", "url": "https://refl.blog/2019/06/04/lambda-calculus-with-generalized-abstraction/", "published_at": "2019-06-03T23:03:42+00:00" }, { "id": "01a0dd50-e883-711e-8a10-99415041390d", "title": "Writing a lambda calculus type-checker in Haskell", "url": "https://refl.blog/2019/03/21/writing-a-lambda-calculus-type-checker-in-haskell/", "published_at": "2019-03-21T16:07:37+00:00" }, { "id": "01a0dd50-e883-711e-8a10-9941512b2bb5", "title": "Writing a lambda calculus evaluator in Haskell", "url": "https://refl.blog/2019/03/19/writing-a-lambda-calculus-evaluator-in-haskell/", "published_at": "2019-03-19T13:34:05+00:00" }, { "id": "01a0dd65-0fea-7178-8db5-69ab6f745d26", "title": "Writing a simple evaluator and type-checker in Haskell", "url": "https://refl.blog/2019/03/15/writing-a-simple-evaluator-and-type-checker-in-haskell/", "published_at": "2019-03-15T14:00:28+00:00" }, { "id": "01a0dd65-0fea-7178-8db5-69ab6fe4db78", "title": "Igpay Igpay Atinlay", "url": "https://refl.blog/2019/03/04/igpay-igpay-atinlay/", "published_at": "2019-03-03T23:00:24+00:00" }, { "id": "01a0dd65-0fea-7178-8db5-69ab7005d146", "title": "Self-publishing my first book", "url": "https://refl.blog/2019/02/27/self-publishing-my-first-book/", "published_at": "2019-02-27T14:56:52+00:00" }, { "id": "01a0dd65-0fea-7178-8db5-69ab7059a87b", "title": "CoC base terms – Type and Prop", "url": "https://refl.blog/2019/02/21/coc-base-terms-type-and-prop/", "published_at": "2019-02-21T08:15:25+00:00" }, { "id": "01a0dd65-0fea-7178-8db5-69ab70def4d6", "title": "If—", "url": "https://refl.blog/2018/11/25/if/", "published_at": "2018-11-25T10:38:33+00:00" }, { "id": "01a0dd65-0fea-7178-8db5-69ab7133b21e", "title": "Proving Monoids with Idris", "url": "https://refl.blog/2018/11/06/proving-monoids-with-idris/", "published_at": "2018-11-06T19:04:06+00:00" }, { "id": "01a0dd65-0fea-7178-8db5-69ab718b8084", "title": "Partial orders in Idris", "url": "https://refl.blog/2018/10/27/partial-orders-in-idris/", "published_at": "2018-10-27T19:52:36+00:00" }, { "id": "01a0dd65-0fea-7178-8db5-69ab725592c7", "title": "Mathematical structure of `git-bisect`", "url": "https://refl.blog/2018/10/21/mathematical-structure-of-git-bisect/", "published_at": "2018-10-21T09:46:32+00:00" }, { "id": "01a0dd65-0fea-7178-8db5-69ab72df5e30", "title": "Lambda calculus implementation in Scheme", "url": "https://refl.blog/2018/09/17/lambda-calculus-implementation-in-scheme/", "published_at": "2018-09-17T11:57:25+00:00" }, { "id": "01a0dd65-0fea-7178-8db5-69ab732074c6", "title": "Closed-expression of a sum with proof in Idris", "url": "https://refl.blog/2018/09/14/closed-expression-of-a-sum-with-proof-in-idris/", "published_at": "2018-09-14T10:03:34+00:00" }, { "id": "01a0dd6f-23d3-71d3-b26c-f8dc7bc9691e", "title": "Twenties retrospective", "url": "https://refl.blog/2018/09/08/twenties-retrospective/", "published_at": "2018-09-08T10:26:00+00:00" }, { "id": "01a0dd6f-23d3-71d3-b26c-f8dc7c933973", "title": "Proving length of mapped and filtered lists in Idris", "url": "https://refl.blog/2018/08/22/proving-length-of-mapped-and-filtered-lists-in-idris/", "published_at": "2018-08-22T01:42:32+00:00" }, { "id": "01a0dd6f-23d3-71d3-b26c-f8dc7d8ed34c", "title": "Simple theorem prover in Racket", "url": "https://refl.blog/2018/08/07/simple-theorem-prover-in-racket/", "published_at": "2018-08-07T19:27:41+00:00" }, { "id": "01a0dd6f-23d3-71d3-b26c-f8dc7dce4cee", "title": "Effects of Side effects", "url": "https://refl.blog/2018/07/23/effects-of-side-effects/", "published_at": "2018-07-23T13:08:39+00:00" }, { "id": "01a0dd6f-23d3-71d3-b26c-f8dc7e7d7827", "title": "Creating our own ‘struct’ macro in Racket", "url": "https://refl.blog/2018/07/11/creating-our-own-struct-macro-in-racket/", "published_at": "2018-07-11T10:42:30+00:00" }, { "id": "01a0dd6f-23d3-71d3-b26c-f8dc7f63fd8d", "title": "Refactoring using mathematical properties of min", "url": "https://refl.blog/2018/06/15/refactoring-using-mathematical-properties-of-min/", "published_at": "2018-06-15T11:45:57+00:00" }, { "id": "01a0dd6f-23d3-71d3-b26c-f8dc7feb3242", "title": "Dafny – programming language for formal specifications", "url": "https://refl.blog/2018/05/13/dafny-programming-language-for-formal-specifications/", "published_at": "2018-05-13T20:32:21+00:00" }, { "id": "01a0dd6f-23d3-71d3-b26c-f8dc80e4f671", "title": "Lisp interpreter", "url": "https://refl.blog/2018/04/27/lisp-interpreter/", "published_at": "2018-04-27T11:15:22+00:00" }, { "id": "01a0dd6f-23d3-71d3-b26c-f8dc80f68d63", "title": "Why Dependent Types matter", "url": "https://refl.blog/2018/04/18/why-dependent-types-matter/", "published_at": "2018-04-18T19:44:44+00:00" }, { "id": "01a0dd6f-23d3-71d3-b26c-f8dc81e3bd5b", "title": "Finding nth term in a sequence", "url": "https://refl.blog/2018/04/02/finding-nth-term-in-a-sequence/", "published_at": "2018-04-02T22:31:54+00:00" }, { "id": "01a0dd7d-50b1-70f0-a506-3a8d445dcbd0", "title": "Proofs with Idris", "url": "https://refl.blog/2018/03/01/proofs-with-idris/", "published_at": "2018-03-01T21:59:52+00:00" }, { "id": "01a0dd7d-50b1-70f0-a506-3a8d452c718a", "title": "Dependent types in typed Racket", "url": "https://refl.blog/2018/02/22/dependent-types-in-typed-racket/", "published_at": "2018-02-22T14:54:26+00:00" }, { "id": "01a0dd7d-50b1-70f0-a506-3a8d45a9d4c5", "title": "Idris, dependent types and IO", "url": "https://refl.blog/2018/02/20/idris-dependent-types-and-io/", "published_at": "2018-02-20T13:26:39+00:00" }, { "id": "01a0dd7d-50b1-70f0-a506-3a8d45ad72d0", "title": "Type systems and proofs", "url": "https://refl.blog/2018/02/18/type-systems-and-proofs/", "published_at": "2018-02-18T20:51:10+00:00" }, { "id": "01a0dd7d-50b1-70f0-a506-3a8d4680a2b9", "title": "Top 3 applications I mostly use", "url": "https://refl.blog/2018/02/01/top-3-applications-i-mostly-use/", "published_at": "2018-02-01T09:54:53+00:00" }, { "id": "01a0dd7d-50b1-70f0-a506-3a8d4729e0e3", "title": "Associativity of Elvis operator", "url": "https://refl.blog/2018/01/31/associativity-of-elvis-operator/", "published_at": "2018-01-31T08:51:47+00:00" }, { "id": "01a0dd7d-50b1-70f0-a506-3a8d481fe3b2", "title": "Metamath", "url": "https://refl.blog/2017/12/17/metamath/", "published_at": "2017-12-17T00:58:48+00:00" }, { "id": "01a0dd7d-50b1-70f0-a506-3a8d4898af5d", "title": "Calculus of Constructions", "url": "https://refl.blog/2017/12/14/calculus-of-constructions/", "published_at": "2017-12-14T16:28:33+00:00" }, { "id": "01a0dd7d-50b1-70f0-a506-3a8d493cb8cd", "title": "Coq to Haskell", "url": "https://refl.blog/2017/12/12/coq-to-haskell/", "published_at": "2017-12-12T16:19:49+00:00" }, { "id": "01a0dd7d-50b1-70f0-a506-3a8d49aaf30a", "title": "MU puzzle", "url": "https://refl.blog/2017/12/07/mu-puzzle/", "published_at": "2017-12-07T21:13:33+00:00" }, { "id": "01a0dd90-804b-73b9-a4f7-d6fc12e08402", "title": "Formal systems", "url": "https://refl.blog/2017/12/06/formal-systems/", "published_at": "2017-12-06T06:42:16+00:00" }, { "id": "01a0dd90-804b-73b9-a4f7-d6fc132bf8b9", "title": "Intuitionistic logic", "url": "https://refl.blog/2017/12/05/intuitionistic-logic/", "published_at": "2017-12-04T23:24:20+00:00" }, { "id": "01a0dd90-804b-73b9-a4f7-d6fc13faa491", "title": "Hierarchy of logical systems", "url": "https://refl.blog/2017/12/04/hierarchy-of-logical-systems/", "published_at": "2017-12-04T11:45:15+00:00" }, { "id": "01a0dd90-804b-73b9-a4f7-d6fc148584c9", "title": "Curry–Howard correspondence", "url": "https://refl.blog/2017/11/27/curry-howard-correspondence/", "published_at": "2017-11-27T17:01:49+00:00" }, { "id": "01a0dd90-804b-73b9-a4f7-d6fc156d5259", "title": "Code checklist", "url": "https://refl.blog/2017/11/16/code-checklist/", "published_at": "2017-11-16T12:56:14+00:00" }, { "id": "01a0dd90-804b-73b9-a4f7-d6fc15791677", "title": "Induction with Coq", "url": "https://refl.blog/2017/11/09/induction-with-coq/", "published_at": "2017-11-09T16:43:58+00:00" }, { "id": "01a0dd90-804b-73b9-a4f7-d6fc15d9ebe2", "title": "More proofs and tactics with Coq", "url": "https://refl.blog/2017/11/07/more-proofs-and-tactics-with-coq/", "published_at": "2017-11-07T16:49:11+00:00" }, { "id": "01a0dd90-804b-73b9-a4f7-d6fc167b2e22", "title": "My first proofs in Coq", "url": "https://refl.blog/2017/11/05/my-first-proofs-in-coq/", "published_at": "2017-11-05T14:56:33+00:00" }, { "id": "01a0dd90-804b-73b9-a4f7-d6fc16a37111", "title": "My first GM experience", "url": "https://refl.blog/2017/09/20/my-first-gm-experience/", "published_at": "2017-09-20T12:00:39+00:00" }, { "id": "01a0dd90-804b-73b9-a4f7-d6fc172192be", "title": "Recursive and iterative processes and procedures", "url": "https://refl.blog/2017/09/05/recursive-and-iterative-processes-and-procedures/", "published_at": "2017-09-05T19:50:15+00:00" } ] posts Claim your blog

Back to refl.blog

Blog · corpus.blog/blogs/refl.blog/posts

refl.blog

refl.blog

2021

The Queen’s Gambit original ↗

30 Sept 2021

Thinking, Fast & Slow Summary original ↗

22 Sept 2021

Closed-expression of a sum with proof in Coq original ↗

20 Sept 2021

Bobby Fischer Teaches Chess Summary original ↗

12 Sept 2021

Reflections on anxiety original ↗

7 Aug 2021

Re-inventing the Monad wheel original ↗

7 Jun 2021

Algorithmic puzzle: Continuous Increasing Subsequences original ↗

9 Apr 2021

Capturing Number Theory in Haskell original ↗

5 Apr 2021

Performant implementation of pagination on Cartesian products original ↗

30 Mar 2021

Towards Hoare logic for a small imperative language in Haskell original ↗

18 Jan 2021

Reflecting on my FTH rotation original ↗

15 Jan 2021

2020

Advent of Code #13 original ↗

24 Dec 2020

Haskell memoization and evaluation model original ↗

11 Dec 2020

Advent of Code #8 original ↗

10 Dec 2020

Diversity and Bias original ↗

22 Oct 2020

Proof: One Sunday every 7 days original ↗

17 Oct 2020

On faith, unbelief, and doubt original ↗

9 Sept 2020

Tenses original ↗

3 Sept 2020

A simple Constraint Programming implementation original ↗

22 Aug 2020

Superliminal game overview original ↗

21 Aug 2020

Proofs and computation with trees original ↗

20 Jun 2020

Deriving a Quine in a Lisp original ↗

24 Apr 2020

Equational reasoning in Racket original ↗

10 Apr 2020

Encoding probability and random variables in Racket original ↗

5 Apr 2020

Stay Home original ↗

14 Mar 2020

Formalization of Boolean algebra pt. 2 original ↗

1 Feb 2020

Introduction and formalization of Boolean algebra original ↗

31 Jan 2020

Wisdom of the crowd exercise original ↗

25 Jan 2020

Dafny proof to the Container With Most Water Problem original ↗

5 Jan 2020

2019

GEB: An EGB overview (Part I)original ↗

30 Dec 2019

Infinite power towers original ↗

10 Dec 2019

Idea: news diversity original ↗

18 Nov 2019

Formalizing expressiveness of line editors original ↗

9 Nov 2019

Proving Groups with Idris original ↗

6 Nov 2019

A8c team meetup Athens, 2019 original ↗

4 Nov 2019

Metapost: Tuply singleton – Freedom of creativity original ↗

19 Oct 2019

Tuply singleton v3 (with proof)original ↗

11 Oct 2019

Tuply singleton v2 original ↗

9 Oct 2019

Tuply singleton original ↗

6 Oct 2019

One plus one equals two original ↗

20 Sept 2019

Meet them all original ↗

15 Sept 2019

Abstraction and generalization of objects original ↗

8 Aug 2019

Generalized average original ↗

5 Aug 2019

Arithmetic on Algebraic Data Types original ↗

30 Jul 2019

Brief introduction to Machine Learning with Gradient Descent original ↗

10 Jul 2019

Naive Set Theory summary original ↗

25 Jun 2019

Customer-driven engineering original ↗

10 Jun 2019

Lambda calculus with generalized abstraction original ↗

3 Jun 2019

Writing a lambda calculus type-checker in Haskell original ↗

21 Mar 2019

Writing a lambda calculus evaluator in Haskell original ↗

19 Mar 2019

Writing a simple evaluator and type-checker in Haskell original ↗

15 Mar 2019

Igpay Igpay Atinlay original ↗

3 Mar 2019

Self-publishing my first book original ↗

27 Feb 2019

CoC base terms – Type and Prop original ↗

21 Feb 2019

2018

If—original ↗

25 Nov 2018

Proving Monoids with Idris original ↗

6 Nov 2018

Partial orders in Idris original ↗

27 Oct 2018

Mathematical structure of `git-bisect`original ↗

21 Oct 2018

Lambda calculus implementation in Scheme original ↗

17 Sept 2018

Closed-expression of a sum with proof in Idris original ↗

14 Sept 2018

Twenties retrospective original ↗

8 Sept 2018

Proving length of mapped and filtered lists in Idris original ↗

22 Aug 2018

Simple theorem prover in Racket original ↗

7 Aug 2018

Effects of Side effects original ↗

23 Jul 2018

Creating our own ‘struct’ macro in Racket original ↗

11 Jul 2018

Refactoring using mathematical properties of min original ↗

15 Jun 2018

Dafny – programming language for formal specifications original ↗

13 May 2018

Lisp interpreter original ↗

27 Apr 2018

Why Dependent Types matter original ↗

18 Apr 2018

Finding nth term in a sequence original ↗

2 Apr 2018

Proofs with Idris original ↗

1 Mar 2018

Dependent types in typed Racket original ↗

22 Feb 2018

Idris, dependent types and IO original ↗

20 Feb 2018

Type systems and proofs original ↗

18 Feb 2018

Top 3 applications I mostly use original ↗

1 Feb 2018

Associativity of Elvis operator original ↗

31 Jan 2018

2017

Metamath original ↗

17 Dec 2017

Calculus of Constructions original ↗

14 Dec 2017

Coq to Haskell original ↗

12 Dec 2017

MU puzzle original ↗

7 Dec 2017

Formal systems original ↗

6 Dec 2017

Intuitionistic logic original ↗

4 Dec 2017

Hierarchy of logical systems original ↗

4 Dec 2017

Curry–Howard correspondence original ↗

27 Nov 2017

Code checklist original ↗

16 Nov 2017

Induction with Coq original ↗

9 Nov 2017

More proofs and tactics with Coq original ↗

7 Nov 2017

My first proofs in Coq original ↗

5 Nov 2017

My first GM experience original ↗

20 Sept 2017

Recursive and iterative processes and procedures original ↗

5 Sept 2017