Howdy! Here are a few of my projects. I hope you find them enjoyable!
Noah was born on July 24th, 2007. He loves to sing songs, read books, play games, and go to the park.
... and a ton of other pictures and movies.
CIRC (Compiler IR Compiler) is a framework similar to Nanopass for describing compilers as a sequence of small datatype transformations. I am currently using CIRC for building the Breeze compiler. Breeze is a dynamically typed programming language with fine-grained, dynamic information flow control.
ImProve is an imperative programming language nested in Haskell for high assurance embedded applications. ImProve uses infinite state, unbounded model checking to verify programs adhere to specifications. At Eaton, we use ImProve to design and verify critical aspects of embedded software that control hydraulic hybrid vehicles.
Atom is a Haskell DSL for designing hard real-time embedded software. At Eaton, we use it for automotive control systems. Based on guarded atomic actions, and similar to software transactional memory, Atom enables highly concurrent programming without the need for mutex locking. In addition, Atom performs compile-time task scheduling and generates code with deterministic execution time and constant memory use, simplifying the process of timing verification and memory consumption in hard realtime applications. Without mutex locking and run-time task scheduling, Atom can eliminate the need and overhead of RTOSs for many embedded applications.
Mecha is a constructive solid geometry modeling language embedded in Haskell. Mecha compiles to POV-Ray and OpenSCAD for visualiation.
A symbol library to diagram hydraulic systems with gschem schematic capture.
A Haskell library to parse and generate VCD files. Though intended for Verilog simulation, we found VCD great for logging and viewing live vehicle data transmitted over a CAN bus.
A Haskell library for instruction set simulation (ISS) and static analysis on PowerPC machine code.
A Makefile and collection of patches to build a GCC cross compiler (C, C++, Ada) for bare metal embedded PowerPC targets.
Atom's Formal Verifier (AFV) is model checker that can verify assertions of an iterative C program without test stimulus or simulation. Based on the Yices SMT solver, AFV can reason about programs with both floating point and integral types.
HTZAAR is an implementation of TZAAR, a 2-player abstract strategy game designed by Kris Burm for the GIPF series of games. HTZAAR currently has a very weak AI, but provides a reasonable interface for creating new AI strategies. HTZAAR can also pit AI versus AI.
Confluence is a functional hardware description language.
HDCaml is an HDL embedded in Objective Caml.