Chris Henson
@chenson.bsky.social
CS PhD student @ Drexel University. Types, categories, and verification. Collector of retro computers and vintage books. Formerly Quant Finance at Bank of America.
I wrote a short blog post "The Interplay Between Metaprogramming and Computation in Lean": chrishenson.net/posts/2025-0...
Chris Henson - The Interplay Between Metaprogramming and Computation in Lean
chrishenson.net
June 28, 2025 at 5:09 PM
I wrote a short blog post "The Interplay Between Metaprogramming and Computation in Lean": chrishenson.net/posts/2025-0...
I've used quiver for my upcoming candidacy exam paper and highly recommended it. Easy to use, and every diagram comes with a link that encodes the diagram. Very nice feature for making edits later.
"Quiver: a modern commutative diagram editor"
@elliot.website This seems like your type of thing.
Source code: github.com/varkor/quiver
@elliot.website This seems like your type of thing.
Source code: github.com/varkor/quiver
December 27, 2024 at 7:22 PM
I've used quiver for my upcoming candidacy exam paper and highly recommended it. Easy to use, and every diagram comes with a link that encodes the diagram. Very nice feature for making edits later.
A few interesting finds at used bookstores today.
December 20, 2024 at 11:08 PM
A few interesting finds at used bookstores today.
My lack of Advent of Code posting is because I've gotten completely sniped into porting Rust's pathfinding crate to Lean, including an implementation of insertion-order preserving hashmaps. If I get it finished and cleaned up over the holiday, I'll be sure to share!
December 20, 2024 at 12:42 AM
My lack of Advent of Code posting is because I've gotten completely sniped into porting Rust's pathfinding crate to Lean, including an implementation of insertion-order preserving hashmaps. If I get it finished and cleaned up over the holiday, I'll be sure to share!
Reposted by Chris Henson
I wanted to answer this but was too lazy and got scooped!
proofassistants.stackexchange.com/q/4526
It's a cool way to use canonicity to give *conservativity* results: a bunch of stuff to add to your logic without making it less trustworthy.
This is one of the first applications of canonicity!
proofassistants.stackexchange.com/q/4526
It's a cool way to use canonicity to give *conservativity* results: a bunch of stuff to add to your logic without making it less trustworthy.
This is one of the first applications of canonicity!
Proving that negative axioms don't break canonicity
In Negative consistent axioms can be postulatedwithout loss of canonicity, the authors show that if $\lnot P$ is a consistent axiom with MLTT, then MLTT+$\lnot P$ still has canonicity of $\mathbb N$.
proofassistants.stackexchange.com
December 14, 2024 at 9:02 PM
I wanted to answer this but was too lazy and got scooped!
proofassistants.stackexchange.com/q/4526
It's a cool way to use canonicity to give *conservativity* results: a bunch of stuff to add to your logic without making it less trustworthy.
This is one of the first applications of canonicity!
proofassistants.stackexchange.com/q/4526
It's a cool way to use canonicity to give *conservativity* results: a bunch of stuff to add to your logic without making it less trustworthy.
This is one of the first applications of canonicity!
Feels a bit odd to post this here too, but I added a short blog post to my site about the ways Twitter has affected my life and career.
chrishenson.net/posts/2024-1...
chrishenson.net/posts/2024-1...
Chris Henson - How Twitter Shaped My Life
chrishenson.net
December 14, 2024 at 5:13 PM
Feels a bit odd to post this here too, but I added a short blog post to my site about the ways Twitter has affected my life and career.
chrishenson.net/posts/2024-1...
chrishenson.net/posts/2024-1...
Day 14 of #AdventofCode in Lean: github.com/chenson2018/...
Nothing too notable, except for being one of the days with a visual element that sometimes generates a bit of controversy.
Nothing too notable, except for being one of the days with a visual element that sometimes generates a bit of controversy.
advent-of-code/2024/lean/AoC/Day14.lean at main · chenson2018/advent-of-code
Contribute to chenson2018/advent-of-code development by creating an account on GitHub.
github.com
December 14, 2024 at 11:03 AM
Day 14 of #AdventofCode in Lean: github.com/chenson2018/...
Nothing too notable, except for being one of the days with a visual element that sometimes generates a bit of controversy.
Nothing too notable, except for being one of the days with a visual element that sometimes generates a bit of controversy.
Day 13 of #AdventofCode in Lean: github.com/chenson2018/...
Just some algebra today. I spent a while fiddling with Diophantine equations, I was disappointed they weren't needed.
Just some algebra today. I spent a while fiddling with Diophantine equations, I was disappointed they weren't needed.
advent-of-code/2024/lean/AoC/Day13.lean at main · chenson2018/advent-of-code
Contribute to chenson2018/advent-of-code development by creating an account on GitHub.
github.com
December 13, 2024 at 2:53 PM
Day 13 of #AdventofCode in Lean: github.com/chenson2018/...
Just some algebra today. I spent a while fiddling with Diophantine equations, I was disappointed they weren't needed.
Just some algebra today. I spent a while fiddling with Diophantine equations, I was disappointed they weren't needed.
Day 11 of #AdventofCode in Lean: github.com/chenson2018/...
One day lag here because I really got into this problem! I defined memoization as a state monad, along with a memoized map function that folds a hashmap over a list.
One day lag here because I really got into this problem! I defined memoization as a state monad, along with a memoized map function that folds a hashmap over a list.
advent-of-code/2024/lean/AoC/Day11.lean at main · chenson2018/advent-of-code
Contribute to chenson2018/advent-of-code development by creating an account on GitHub.
github.com
December 12, 2024 at 12:15 PM
Day 11 of #AdventofCode in Lean: github.com/chenson2018/...
One day lag here because I really got into this problem! I defined memoization as a state monad, along with a memoized map function that folds a hashmap over a list.
One day lag here because I really got into this problem! I defined memoization as a state monad, along with a memoized map function that folds a hashmap over a list.
I love seeing the language distribution in my Advent of Code repo change over the years
December 10, 2024 at 8:20 AM
I love seeing the language distribution in my Advent of Code repo change over the years
Day 10 of #AdventofCode in Lean: github.com/chenson2018/...
Very straightforward, not much to say. One of those days where part two was one a one line change from part one.
Very straightforward, not much to say. One of those days where part two was one a one line change from part one.
advent-of-code/2024/lean/AoC/Day10.lean at main · chenson2018/advent-of-code
Contribute to chenson2018/advent-of-code development by creating an account on GitHub.
github.com
December 10, 2024 at 8:17 AM
Day 10 of #AdventofCode in Lean: github.com/chenson2018/...
Very straightforward, not much to say. One of those days where part two was one a one line change from part one.
Very straightforward, not much to say. One of those days where part two was one a one line change from part one.
Day 9 of #AdventofCode in Lean: github.com/chenson2018/...
Nothing conceptually difficult, but lots of bookkeeping here that took a while to get right and could probably be a bit cleaner.
Nothing conceptually difficult, but lots of bookkeeping here that took a while to get right and could probably be a bit cleaner.
advent-of-code/2024/lean/AoC/Day09.lean at main · chenson2018/advent-of-code
Contribute to chenson2018/advent-of-code development by creating an account on GitHub.
github.com
December 9, 2024 at 12:35 PM
Day 9 of #AdventofCode in Lean: github.com/chenson2018/...
Nothing conceptually difficult, but lots of bookkeeping here that took a while to get right and could probably be a bit cleaner.
Nothing conceptually difficult, but lots of bookkeeping here that took a while to get right and could probably be a bit cleaner.
Day 8 of #AdventofCode in Lean: github.com/chenson2018/...
Just some mildly tedious slope calculations today. I'll be curious to see more clever solutions than mine.
I left one partial def because it was tedious to prove that a line stays bounded in a square, will likely revisit that later.
Just some mildly tedious slope calculations today. I'll be curious to see more clever solutions than mine.
I left one partial def because it was tedious to prove that a line stays bounded in a square, will likely revisit that later.
advent-of-code/2024/lean/AoC/Day08.lean at main · chenson2018/advent-of-code
Contribute to chenson2018/advent-of-code development by creating an account on GitHub.
github.com
December 8, 2024 at 7:43 AM
Day 8 of #AdventofCode in Lean: github.com/chenson2018/...
Just some mildly tedious slope calculations today. I'll be curious to see more clever solutions than mine.
I left one partial def because it was tedious to prove that a line stays bounded in a square, will likely revisit that later.
Just some mildly tedious slope calculations today. I'll be curious to see more clever solutions than mine.
I left one partial def because it was tedious to prove that a line stays bounded in a square, will likely revisit that later.
The slowness was bothering me, so I rewrote the combinations code. Reduced runtime from ~40s to ~2s. Relies on the fact the the calculations are cumulative.
Day 7 of #AdventofCode in Lean: github.com/chenson2018/...
A little slow (takes ~40s for both parts), but I think that this is because there is not an extern base 10 logarithm and me not being too careful with how I generate combinations. Otherwise a pretty straightforward day.
A little slow (takes ~40s for both parts), but I think that this is because there is not an extern base 10 logarithm and me not being too careful with how I generate combinations. Otherwise a pretty straightforward day.
advent-of-code/2024/lean/AoC/Day07.lean at main · chenson2018/advent-of-code
Contribute to chenson2018/advent-of-code development by creating an account on GitHub.
github.com
December 7, 2024 at 5:55 PM
The slowness was bothering me, so I rewrote the combinations code. Reduced runtime from ~40s to ~2s. Relies on the fact the the calculations are cumulative.
Reposted by Chris Henson
PLsky: what are some topics to cover in an "Advanced tools in PL" class? My picks:
- Metaprogramming Systems (macros, user-scheduling)
- Type systems (Graded modal, dependent, substructural)
- Program logics (hoare, incorrectness)
What else?
- Metaprogramming Systems (macros, user-scheduling)
- Type systems (Graded modal, dependent, substructural)
- Program logics (hoare, incorrectness)
What else?
December 7, 2024 at 3:02 PM
PLsky: what are some topics to cover in an "Advanced tools in PL" class? My picks:
- Metaprogramming Systems (macros, user-scheduling)
- Type systems (Graded modal, dependent, substructural)
- Program logics (hoare, incorrectness)
What else?
- Metaprogramming Systems (macros, user-scheduling)
- Type systems (Graded modal, dependent, substructural)
- Program logics (hoare, incorrectness)
What else?
Day 7 of #AdventofCode in Lean: github.com/chenson2018/...
A little slow (takes ~40s for both parts), but I think that this is because there is not an extern base 10 logarithm and me not being too careful with how I generate combinations. Otherwise a pretty straightforward day.
A little slow (takes ~40s for both parts), but I think that this is because there is not an extern base 10 logarithm and me not being too careful with how I generate combinations. Otherwise a pretty straightforward day.
advent-of-code/2024/lean/AoC/Day07.lean at main · chenson2018/advent-of-code
Contribute to chenson2018/advent-of-code development by creating an account on GitHub.
github.com
December 7, 2024 at 11:50 AM
Day 7 of #AdventofCode in Lean: github.com/chenson2018/...
A little slow (takes ~40s for both parts), but I think that this is because there is not an extern base 10 logarithm and me not being too careful with how I generate combinations. Otherwise a pretty straightforward day.
A little slow (takes ~40s for both parts), but I think that this is because there is not an extern base 10 logarithm and me not being too careful with how I generate combinations. Otherwise a pretty straightforward day.
Day 6 of #AdventofCode in Lean: github.com/chenson2018/...
First day that required a smidge of optimization. A typo in part 1 wasted a lot of time. I actually solved it by hand first! I did a bit of a hack for part 2 because properly counting duplicate states seemed like a hassle.
First day that required a smidge of optimization. A typo in part 1 wasted a lot of time. I actually solved it by hand first! I did a bit of a hack for part 2 because properly counting duplicate states seemed like a hassle.
advent-of-code/2024/lean/AoC/Day06.lean at main · chenson2018/advent-of-code
Contribute to chenson2018/advent-of-code development by creating an account on GitHub.
github.com
December 6, 2024 at 11:59 AM
Day 6 of #AdventofCode in Lean: github.com/chenson2018/...
First day that required a smidge of optimization. A typo in part 1 wasted a lot of time. I actually solved it by hand first! I did a bit of a hack for part 2 because properly counting duplicate states seemed like a hassle.
First day that required a smidge of optimization. A typo in part 1 wasted a lot of time. I actually solved it by hand first! I did a bit of a hack for part 2 because properly counting duplicate states seemed like a hassle.
Day 5 of #AdventofCode in Lean: github.com/chenson2018/...
One of my favorite days so far, came out very cleanly. Having quicksort in the language is nice. I enjoyed writing the function to get the middle of an Array with a provably correct index, though ran into some decidable equality trickiness.
One of my favorite days so far, came out very cleanly. Having quicksort in the language is nice. I enjoyed writing the function to get the middle of an Array with a provably correct index, though ran into some decidable equality trickiness.
advent-of-code/2024/lean/AoC/Day05.lean at main · chenson2018/advent-of-code
Contribute to chenson2018/advent-of-code development by creating an account on GitHub.
github.com
December 5, 2024 at 8:32 AM
Day 5 of #AdventofCode in Lean: github.com/chenson2018/...
One of my favorite days so far, came out very cleanly. Having quicksort in the language is nice. I enjoyed writing the function to get the middle of an Array with a provably correct index, though ran into some decidable equality trickiness.
One of my favorite days so far, came out very cleanly. Having quicksort in the language is nice. I enjoyed writing the function to get the middle of an Array with a provably correct index, though ran into some decidable equality trickiness.
Inside of you are two wolves
December 4, 2024 at 4:58 PM
Inside of you are two wolves
Day 4 of #AdventofCode in Lean: github.com/chenson2018/...
I just used a list of lists as a matrix as opposed to something dependently typed, though I did ensure all indexing was checked at least.
For part one, I was pretty happy with my method of getting all diagonals.
I just used a list of lists as a matrix as opposed to something dependently typed, though I did ensure all indexing was checked at least.
For part one, I was pretty happy with my method of getting all diagonals.
advent-of-code/2024/lean/AoC/Day04.lean at main · chenson2018/advent-of-code
Contribute to chenson2018/advent-of-code development by creating an account on GitHub.
github.com
December 4, 2024 at 8:41 AM
Day 4 of #AdventofCode in Lean: github.com/chenson2018/...
I just used a list of lists as a matrix as opposed to something dependently typed, though I did ensure all indexing was checked at least.
For part one, I was pretty happy with my method of getting all diagonals.
I just used a list of lists as a matrix as opposed to something dependently typed, though I did ensure all indexing was checked at least.
For part one, I was pretty happy with my method of getting all diagonals.
Day 3 of #AdventofCode in Lean: github.com/chenson2018/...
It is redundant with the actual monadic parsing, but I played around a bit with the regex package today. Pretty painless experience, I was pleasantly surprised. Not much else of note.
It is redundant with the actual monadic parsing, but I played around a bit with the regex package today. Pretty painless experience, I was pleasantly surprised. Not much else of note.
advent-of-code/2024/lean/AoC/Day03.lean at main · chenson2018/advent-of-code
Contribute to chenson2018/advent-of-code development by creating an account on GitHub.
github.com
December 3, 2024 at 7:41 AM
Day 3 of #AdventofCode in Lean: github.com/chenson2018/...
It is redundant with the actual monadic parsing, but I played around a bit with the regex package today. Pretty painless experience, I was pleasantly surprised. Not much else of note.
It is redundant with the actual monadic parsing, but I played around a bit with the regex package today. Pretty painless experience, I was pleasantly surprised. Not much else of note.
I made a list of people I've seen doing Advent of Code in Lean this year. Please let me know if I missed anyone!
bsky.app/profile/did:...
bsky.app/profile/did:...
December 3, 2024 at 3:19 AM
I made a list of people I've seen doing Advent of Code in Lean this year. Please let me know if I missed anyone!
bsky.app/profile/did:...
bsky.app/profile/did:...
Advent of Code, Day 2, again in Lean: github.com/chenson2018/...
Still early days, not too interesting. `List.eraseIdx` worked well for the part 2. I though about doing removals from the diff list instead of the original (then adjusting by the removed diff), but it's so quick that I didn't bother.
Still early days, not too interesting. `List.eraseIdx` worked well for the part 2. I though about doing removals from the diff list instead of the original (then adjusting by the removed diff), but it's so quick that I didn't bother.
advent-of-code/2024/lean/AoC/Day02.lean at main · chenson2018/advent-of-code
Contribute to chenson2018/advent-of-code development by creating an account on GitHub.
github.com
December 2, 2024 at 6:02 AM
Advent of Code, Day 2, again in Lean: github.com/chenson2018/...
Still early days, not too interesting. `List.eraseIdx` worked well for the part 2. I though about doing removals from the diff list instead of the original (then adjusting by the removed diff), but it's so quick that I didn't bother.
Still early days, not too interesting. `List.eraseIdx` worked well for the part 2. I though about doing removals from the diff list instead of the original (then adjusting by the removed diff), but it's so quick that I didn't bother.
As promised, doing Advent of Code in Lean this year. Link in the replies to appease the algorithm (does that apply here too??):
December 1, 2024 at 8:21 AM
As promised, doing Advent of Code in Lean this year. Link in the replies to appease the algorithm (does that apply here too??):
Reposted by Chris Henson
"The Haskell inlining and specialization FAQ" by @gabriella439.bsky.social
www.haskellforall.com/2024/11/the-...
#Haskell
www.haskellforall.com/2024/11/the-...
#Haskell
The Haskell inlining and specialization FAQ
The Haskell inlining and specialization FAQ This is a post is an FAQ answering the most common questions peo...
www.haskellforall.com
November 26, 2024 at 10:33 PM
"The Haskell inlining and specialization FAQ" by @gabriella439.bsky.social
www.haskellforall.com/2024/11/the-...
#Haskell
www.haskellforall.com/2024/11/the-...
#Haskell