
Recent Posts
Recent Comments
sanjoyd on Faking Dependent Types in… drocta on Faking Dependent Types in… Matt on Faking Dependent Types in… Francis Kim on Faking Dependent Types in… Anurag Bishnoi on On why religion is a double… Archives
Categories
Meta
Category Archives: Computers
Color Schemes
I wrote a new minimalist color scheme (for emacs) today. If you’re into that sort of thing, the code is on github, and down below is a screenshot. Advertisements
A JIT Compiler for Brainf*ck
I recently read this article by Josh Haberman where he demonstrates a JIT for the Brainf*ck language (henceforth referred to as BF). However it wasn’t very different from a regular AOT compiler — the entire BF script is read in … Continue reading
Lambda Calculus for the Imperative Programmer I
This post is first in a series of articles on lambda calculus. You can see the whole series by looking up the tag lcip. The Untyped Lambda Calculus At the very core, the untyped lambda calculus (referred to as λ … Continue reading
Lockfree programming, first steps: mostly lockfree fixedsize vector
I recently got interested in lockfree programming techniques, and began playing with the idea of a lockfree, fixed size vector. While the final result isn’t completely lockfree, it is an optimization over a naively locked version. The following is a … Continue reading
Peeking inside LuaJIT
LuaJIT is a highperformance virtual machine for Lua. I’ve recently started playing with it and this blog post talks about what I’ve discovered so far. LuaJIT is a tracing JIT as opposed to a method JIT — it works not … Continue reading
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, lambdacalculus, and static type systems, using the Coq proof assistant”. This post is an … Continue reading
Posted in Computers
Tagged agda, cic, classical logic, coq, haskell, logic, theorem proving
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 agda, function programming, haskell, static analysis, TAL, typed assembly, types
Leave a comment