Tagged "Coq"
-
A Verified Evaluator for the Untyped Concatenative Calculus
6826 words, about 33 minutes to read.
Earlier, I wrote an article in which I used Coq to encode the formal semantics of Dawn’s Untyped Concatenative Calculus , and to prove a few things about the mini-language. ...
-
Formalizing Dawn in Coq
4373 words, about 21 minutes to read.
The Foundations of Dawn article came up on Lobsters recently. In this article, the author of Dawn defines a core calculus for the language, and provides its semantics. ...
-
Advent of Code in Coq - Day 8
8609 words, about 41 minutes to read.
Huh? We’re on day 8? What happened to days 2 through 7? Well, for the most part, I didn’t think they were that interesting from the Coq point of view. ...
-
Advent of Code in Coq - Day 1
3515 words, about 17 minutes to read.
The first puzzle of this year’s Advent of Code was quite simple, which gave me a thought: “Hey, this feels within reach for me to formally verify! ...
-
Proof of Inductive Palindrome Definition in Coq
1408 words, about 7 minutes to read.
Going through the Software Foundations textbook, I found an exercise which I really enjoyed solving. This exercise was to define an inductive property that holds iff a list is a palindrome. ...