David Thrane Christiansen

czm-lean4.el. Some embellishments for lean4-mode

Calligraphic-Rulings. A simple program to create ruling pages for English calligraphy

hs-opt-handbook.github.io. The Haskell Optimization Handbook

xournalpp. Xournal++ is a handwriting notetaking software with PDF annotation support. Written in C++ with GTK3, supporting Linux (e.g. Ubuntu, Debian, Arch, SUSE), macOS and Windows 10. Supports pen input from devices such as Wacom Tablets.

smalltt. Demo for high-performance type theory elaboration

idris-malfunction. Experimental Malfunction backend for Idris

miniprl. A small implementation of a proof refinement logic.

racket-poppler. Racket bindings for Poppler (library for reading and generating pdfs)

JonPRL. An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]

Brainfuck. Brainfuck formalized in Coq

QFeldspar-Idris. A port of QFeldspar to Idris

gist.el. Yet another Emacs paste mode, this one for Gist.

IHaskell. A Haskell kernel for the Jupyter project.

ml-mukanren. microkanren in sml

idris-xml. A simple XML module for Idris.

curses-idris. Curses bindings package for Idris

martin-lof. papers of Per Martin Löf

copatterns. A repository for a project concerning copatterns.

atom-language-idris. A Idris Mode for Atom.io

pa-applet. PulseAudio control applet

quantities. Type-safe physical computations and unit conversions in Idris ⚖ 🌡 ⏲ 🔋 📐

structured-haskell-mode. Structured editing minor mode for Haskell in Emacs

idris-demos. Collection of Idris tests and demonstration programs

circe. Circe, a Client for IRC in Emacs

dtip. Dependently Typed Idris Programming language

deuce. Deuce is (not yet) Emacs under Clojure

lamdu. lamdu - towards the next generation IDE

idris-mode. Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.

FormHelper. Create forms and validations for Scala and Javascript with this small form dsl language.

tiny-dependent-types. A very simple implementation of a little dependently typed language

Idris-dev. A Dependently Typed Functional Programming Language

aml-mode. AML mode for Emacs

beamerOerestad. Unofficial IT University of Copenhagen beamer style

fflat-mdsliterals. Extension of Fb with support for modular structured data literals (like XML, JSON, YAML etc.)

scalacheck. A powerful tool for automatic unit testing

typesearch. Scala

beamerOerestad. Unofficial IT University of Copenhagen beamer style

bibtex-kindle. Some elisp code which uses bibtex to export pdfs to kindle (metadata and collections)

Idris-dev. A Dependently Typed Functional Programming Language

taffybar. A gtk based status bar for tiling window managers such as XMonad

scalacheck. Property-based testing for Scala

emacs-bash-completion. Add programmable bash completion to Emacs shell-mode

coqoon. eclipse plugin to support side-by-side proofs and code

simply_lift. The Simply Lift book

extradoc. An extended version of Scala's scaladoc command

colladoc. Web application allowing to edit Scala symbols documentation

scala-doc-search. A Hoogle clone for Scaladoc

writegood-mode. Minor mode for Emacs to improve English writing