Tag Archives: agda

Classical Axioms in Coq

Posted on September 18, 2012 by sanjoyd

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.

Posted on September 15, 2012 by sanjoyd

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

Logic Puzzles in Agda

Posted on September 6, 2012 by sanjoyd

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

First steps with Agda: provable factoring

Posted on August 19, 2012 by sanjoyd

In my last post we looked at the problem of factoring an integer. We ran into an issue with the termination checker and resolved it by wrapping the recursion into a separate inductive data-type that made it explicit. The idiom … Continue reading →

Posted in Computers | Tagged , , | Leave a comment