topolog. a programming system (within Coq) for continuous spaces
topolog is a work-in-progress programming language, embedded in Coq, whose types are spaces and whose expressions are continuous maps. Its execution is based on formal topology, a constructive theory of topology.
Idris :search. search for Idris terms using an approximate type signature
Idris is a purely functional programming language with dependent types. Like Hoogle for Haskell, :search allows programmers to search for terms using an approximate type signature. :search returns terms with types that isomorphic, more general, or more specific than the searched type, and conveys this relation.
LinAlg. Haskell libraries for numerical linear algebra with strong types
- LinAlg (Github, Haddock docs) provides an interface for specifying numeric linear algebra computations in a purely functional manner. Array sizes are reflected statically in the types. It has a backend for performing computations on the CPU with hmatrix.
- LinAlg-magma (Github, Haddock docs) provides a GPU-powered backend for LinAlg. It also provides a lower-level API with mutable data structures and destructive operations. This API uses an ST-like interface and uses the type system to allow destructive operations to read from either mutable or immutable structures.
- CUBLAS FFI bindings: Hackage, Github
- MAGMA FFI bindings: Github
HM programming language. a toy functional programming language with a Hindley-Milner like type system that compiles to x64 assembly
This is a toy language that I designed for a Compilers class that I took at GMU. Its features include polymorphic algebraic data types, polymorphic functions, Hindley-Milner type inference, first-class functions, simple pattern matching, and tail-call optimization.
AutoTabber. generates optimal guitar tablature from MIDI files describing guitar pieces
LiveHistogram. display live histograms for data streams in the console
priority-map. mutable heap allowing random access (in Haskell)