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 minilanguage. ...

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. ...