Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
896 Commits 8 Branches 0 Tags 46 MiB
1f01c3caff
Commit Graph

441 Commits

Author SHA1 Message Date
Danila Fedorin
e91b6f692f Publish introducton to SPA in Agda 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-07-06 17:42:44 -07:00
Danila Fedorin
861dafef70 Finish up draft about lattices of finite height. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-07-05 20:43:26 -07:00
Danila Fedorin
388c23c376 Write more on finite height lattices 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-07-05 12:09:29 -07:00
Danila Fedorin
826a16eb66 Start working on part 3 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-06-27 22:26:01 -07:00
Danila Fedorin
4fd6dd5606 Make minor edits to article and update theme 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-06-24 19:59:51 -07:00
Danila Fedorin
b3db25c470 Fix some typos and publish the microfeatures post 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-06-23 18:02:13 -07:00
Danila Fedorin
6a7b6ffc1f Write an article about microfeatures 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-06-23 17:59:03 -07:00
Danila Fedorin
0bf3facf6c Add series navigation before appendix 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-06-19 22:04:01 -07:00
Danila Fedorin
8656985885 Introduce "join" and "meet" as terms 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-06-16 20:12:39 -07:00
Danila Fedorin
1fb7e5ff85 Finish draft of part 2, combining lattices 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-06-16 18:09:56 -07:00
Danila Fedorin
df75d6e017 Slightly expand the draft. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-06-09 19:39:00 -07:00
Danila Fedorin
7b03183e75 Continue expanding on the map draft 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-06-09 18:02:04 -07:00
Danila Fedorin
4c70e61a14 Write some more in combining lattices 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-30 22:41:15 -07:00
Danila Fedorin
8e4759bd2b Start on the navigation links in Agda SPA intro 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-30 20:52:33 -07:00
Danila Fedorin
71c030b947 Slightly tweak wording and front matter in Agda SPA posts 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-30 20:02:49 -07:00
Danila Fedorin
1f3ab5349a Restore the dates in 'learning emulation' to their proper ones. 
I found the original dates using the Wayback machine.

https://web.archive.org/web/20161022053013/https://danilafe.com/

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-30 18:58:38 -07:00
Danila Fedorin
b66c58b68e Lightly edit and publish the Agda+Hugo post 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-30 00:30:05 -07:00
Danila Fedorin
13636a0d29 Write more about Agda+Hugo 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-30 00:13:48 -07:00
Danila Fedorin
6a168f2fe1 Start on a draft about Agda and Hugo 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-25 23:28:18 -07:00
Danila Fedorin
04f12b545d Minor edits to 'lattices 2' 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-25 20:45:19 -07:00
Danila Fedorin
711b01175d Put the number back to what it was 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-24 23:12:27 -07:00
Danila Fedorin
272c2666c5 Inconsequential tweak to test Agda caching in build system 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-24 13:44:34 -07:00
Danila Fedorin
c0f4fe017f Replace absolute links with relrefs 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-22 23:05:11 -07:00
Danila Fedorin
11d726a6ad Fix absolute link in favor of relref 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-22 23:01:26 -07:00
Danila Fedorin
ee8b1f5dc0 Write a bit more, enable support for paragraph links 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-21 19:04:08 -07:00
Danila Fedorin
4938cdaecd Work some more on lattices 2 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-20 22:46:18 -07:00
Danila Fedorin
84f28ae5ce Add tags to Agda articles 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-20 21:46:14 -07:00
Danila Fedorin
58e7a1f2dc Start on a draft of 'combining lattices' 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-20 21:39:03 -07:00
Danila Fedorin
78bba7a0e9 Update the blog for series navigation 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-20 00:37:16 -07:00
Danila Fedorin
9d31764073 Tie up Lattices (1), and plan to write Lattices (2) 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-19 22:29:24 -07:00
Danila Fedorin
60d3b3025a Flesh out the Lattices post some more 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-14 21:43:12 -07:00
Danila Fedorin
1df315612a Update "typesafe interpreter" article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 19:08:17 -07:00
Danila Fedorin
15beddf96b Update btree article with new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 19:07:44 -07:00
Danila Fedorin
20d8b18a9b Update 'stack language recursion' article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 19:07:01 -07:00
Danila Fedorin
53ff0c39e4 Update "search as polynomial" article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 19:06:33 -07:00
Danila Fedorin
357a3bef09 Update the modulo patterns article to use new delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 19:04:08 -07:00
Danila Fedorin
81eef51e88 Update 'math rendering is wrong' to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 19:02:14 -07:00
Danila Fedorin
10dfb2fe49 Update "church encoding" article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 19:01:42 -07:00
Danila Fedorin
ef76149112 Update 'newtype' article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 19:01:08 -07:00
Danila Fedorin
a6a330a78e Update Haskell LSP article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 19:00:23 -07:00
Danila Fedorin
7f4d0df366 Update "catemorphisms" article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:59:54 -07:00
Danila Fedorin
3eddac0a89 Update "proving my compiler incorrect" to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:58:50 -07:00
Danila Fedorin
6e7ac1c1ca Update "I don't like Coq's docs" article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:58:15 -07:00
Danila Fedorin
68d9cf1274 Update 'evaluator for Dawn in Coq' article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:57:15 -07:00
Danila Fedorin
5eb0d1548c Update dawn-in-coq to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:55:59 -07:00
Danila Fedorin
e543904995 Update boolean values article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:54:11 -07:00
Danila Fedorin
ffda1d3235 Moved the bergamot article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:52:21 -07:00
Danila Fedorin
b705aa217c Update "expr pattern in agda" to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:50:56 -07:00
Danila Fedorin
6f20b17948 Update "compiler: polymorphic data types" to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:50:05 -07:00
Danila Fedorin
2fde7e5cf8 Update "compiler: polymorphism" to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:48:34 -07:00
Danila Fedorin
bee06b6731 Update "compiler: compilation" to use new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:43:14 -07:00
Danila Fedorin
d3fa7336a2 Update "compiler: execution" to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:38:05 -07:00
Danila Fedorin
96545a899f Update "compiler: typechecking" to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:33:30 -07:00
Danila Fedorin
6ef5ae2394 Update "types: variables" to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:31:52 -07:00
Danila Fedorin
05a31dd4d4 Update 'compiler: parsing' article to new string literals 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:30:27 -07:00
Danila Fedorin
d9d5c8bf14 Switch 'types: basics' to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:28:36 -07:00
Danila Fedorin
291a1f0178 Update SPA article on Lattices with new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:22:21 -07:00
Danila Fedorin
2547b53aa2 Switch "Homework for an assignment" post 2 to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:20:54 -07:00
Danila Fedorin
409f8b7186 Switch tokenizing article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:20:04 -07:00
Danila Fedorin
189422bf1e Convert AoC Coq article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:16:20 -07:00
Danila Fedorin
befcd3cf98 Add a sidenote about land and lor. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 15:41:50 -07:00
Danila Fedorin
6179c86919 Show the basic Nat lattice. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-12 18:52:26 -07:00
Danila Fedorin
a20fe07a56 Move original 'monotone function' text into new post and heavily rework it 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-12 18:28:44 -07:00
Danila Fedorin
2b5dcf12d7 Rename the SPA intro to have a specific name 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-12 13:50:29 -07:00
Danila Fedorin
5873c1ca96 Write a high-level introduction for the SPA series 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-12 13:49:21 -07:00
Danila Fedorin
c6e2ecb996 Add first section of Agda program analysis article 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-14 22:25:17 -07:00
Danila Fedorin
2130b00752 Narrow some of the tags 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-13 15:59:46 -07:00
Danila Fedorin
474c3a8348 Switch bracket types in Agda expression pattern post 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-13 15:05:37 -07:00
Danila Fedorin
29a18b8b37 Add description to expr_pattern 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-11 23:26:07 -07:00
Danila Fedorin
7d2842fd64 Add article about the 'deeply embedded expression' pattern 2024-03-11 23:15:56 -07:00
Danila Fedorin
266bf9b4cf Add an exercise about conversions to types: basics 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-29 12:47:58 -08:00
Danila Fedorin
a6f3bccf64 Use markdown for exercises, since it works fine out of the box. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-28 16:05:15 -08:00
Danila Fedorin
d7d99205a1 Properly escape < in HTML content. 2023-12-28 00:36:58 -08:00
Danila Fedorin
9f437d5b9f Add a couple of exercises to types: basics. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-28 00:13:13 -08:00
Danila Fedorin
72fb69d87b Make minor changes to types: basics. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-27 23:31:45 -08:00
Danila Fedorin
ed4fcf5e9d Start explaining exercises in types intro. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-27 23:31:28 -08:00
Danila Fedorin
8f2b2addc2 Rename the widget IDs to not include numbers. 2023-12-27 13:16:20 -08:00
Danila Fedorin
e4743bbdef Make some edits to 'types' part 1. 2023-12-26 14:02:48 -08:00
Danila Fedorin
645f2c5c9c Update inference rules to match new Bergamot's single-literal output 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-26 13:21:37 -08:00
Danila Fedorin
16086e79b0 Proofread and publish bergamot post 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-22 22:15:17 -08:00
Danila Fedorin
0c895a2662 Add an initial draft of the Bergamot post. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-22 22:00:06 -08:00
Danila Fedorin
dc9dbe8a0f Update for bergamot requiring an 'input program' too 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-22 16:04:33 -08:00
Danila Fedorin
a83268a6e3 Update use of the bergamot widget 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-21 17:26:19 -08:00
Danila Fedorin
c25f9ad9ae Add the work-in-progress Bergamot widget to the basics page. 2023-11-29 23:21:15 -08:00
Danila Fedorin
3bceab0606 Fix dates 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-10-14 15:58:20 -07:00
Danila Fedorin
c189da3671 Finalize the X Macro article 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-10-14 15:38:54 -07:00
Danila Fedorin
dd232cedb5 Fixup links and add description to X Macros article. 2023-10-09 20:33:21 -07:00
Danila Fedorin
88c5daa561 Add the 'chapel' tag to the alloy article 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-10-09 20:24:19 -07:00
Danila Fedorin
4f281ef108 Add a draft article about X Macros 2023-10-09 20:23:57 -07:00
Danila Fedorin
12aca7ca58 Update the Alloy blogpost to point to the GitHub files. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-10-09 14:41:03 -07:00
Danila Fedorin
6b24d67409 Minor wording updates to the Agda post. 2023-08-31 22:30:36 -07:00
Danila Fedorin
48c3105f42 Finish and publish the IsSomething article 2023-08-31 22:16:26 -07:00
Danila Fedorin
032453c4d0 Add a first draft of the IsSomething article 2023-08-28 23:04:39 -07:00
Danila Fedorin
1f5e38190d Fix DeMorgan's link 2023-06-04 22:03:38 -07:00
Danila Fedorin
250884c7bc Edit and publish Alloy article 2023-06-04 21:56:45 -07:00
Danila Fedorin
5910ce7980 Say screw it and publish polynomial article 2023-05-22 21:42:32 -07:00
Danila Fedorin
00bec06012 Make some edits to the polynomial draft 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-05-22 20:44:50 -07:00
Danila Fedorin
54dccdbc7d Fix accidentally lowercased shortcode 2023-05-14 21:23:22 -07:00
Danila Fedorin
2bd776ec55 Add a description and disclaimer to the Alloy draft. 2023-05-14 21:18:23 -07:00
Danila Fedorin
23cf7c9e8b Finish initial draft of the Alloy article. 2023-05-14 21:13:23 -07:00