Monthly Archives: September 2012

Classical Axioms in Coq

For the past few days I’ve been working through an amazing text, Software Foundations, which aims to develop “basic concepts of functional programming, logic, operational semantics, lambda-calculus, and static type systems, using the Coq proof assistant”. This post is an … Continue reading

Posted in Computers | Tagged , , , , , , | Leave a comment

Typechecking TAL0 in Agda.

This post is an annotated solution to problem 4.2.11 in the book Advanced Topics in Types and Programming Languages from the chapter Typed Assembly Language by Gerg Morrisett. Introducing TAL0 I’ll do my best to give an informal introduction to … Continue reading

Posted in Computers | Tagged , , , , , , | Leave a comment

Initial Algebras: Part II

In the last post we looked at functor algebras and properties of morphisms (arrows) between them. In this post we’ll explore initial functor algebras (or initial F-Algebras). The Cliffhanger The last episode ended with a question on whether it is … Continue reading

Posted in Computers | Tagged , , , , | Leave a comment

Initial Algebras: Part I

Meta-post This post is light on math and uses Haskell to express formalisms. If you’re clear on what a Functor is, you’re good to go. Functors and Algebras There is this regular old functor, with the type constructor Func. We’ve … Continue reading

Posted in Computers | Tagged , , , , , | 6 Comments

Logic Puzzles in Agda

This post assumes basic knowledge of Agda. A few days ago, Paul Snively published a post which set me thinking on how Agda (which is the closest thing to Coq I have some knowledge of) fares in similar scenarios. Pretty … Continue reading

Posted in Computers | Tagged , , , | Leave a comment