pqnelson

pqnelson's Stars

• jart/sectorlisp

  Bootstrapping LISP in a Boot Sector

  Language:C1.3k321155

• coalton-lang/coalton

  Coalton is an efficient, statically typed functional programming language that supercharges Common Lisp.

  Language:Common Lisp1.2k3143070

• yallop/effects-bibliography

  A collaborative bibliography of work related to the theory and practice of computational effects

  97263484

• augustss/MicroHs

  Haskell implemented with combinators

  Language:Haskell369123925

• antalsz/hs-to-coq

  Convert Haskell source code to Coq source code

  Language:Coq2791614727

• darius/ichbins

  A tiny self-hosting Lisp-to-C compiler

  Language:C23611123

• chriskempson/base16-shell

  Base16 for Shells

  Language:Shell2143038

• blynn/compiler

  The adventures of a Haskell compiler

  Language:Haskell21313416

• chrisdone-archive/duet

  A tiny language, a subset of Haskell aimed at aiding teachers teach Haskell

  Language:Haskell2121007

• diku-dk/smlpkg

  Generic package manager for Standard ML libraries and programs

  Language:Standard ML162945

• mikeshulman/narya

  A proof assistant for higher-dimensional type theory

  Language:OCaml14919510

• vijithassar/lit

  a little preprocessor for literate programming

  Language:Shell119476

• mentat-collective/road-to-reality

  The Road to Reality essay and newsletter source. A journey through computational physics, from eval/apply to the Einstein field equations.

  Language:Clojure9010710

• TiarkRompf/collapsing-towers

  Collapsing Towers of Interpreters

  Language:Coq86906

• slindley/effect-handlers

  Language:Haskell801909

• shwestrick/smlfmt

  A custom parser/auto-formatter for Standard ML

  Language:Standard ML68114715

• ocaml-gospel/cameleer

  A Deductive Verification Tool for OCaml Programs

  Language:OCaml605148

• digama0/mizar-rs

  Alternative Mizar proof checker (http://mizar.org/) written in Rust

  Language:Rust47794

• avikalpg/POPL

  This is a repository for assignments of the course Principles of Programming Languages

  Language:Oz445113

• MizarProject/system

  Language:Pascal36618

• medovina/natty

  Natty is a natural-language proof assistant with an embedded automatic prover for higher-order logic. It is in an early stage of development.

  Language:OCaml35201

• JoshuaGrams/pep

  A Pint-sized Earley Parser

  Language:HTML34704

• naproche/naproche

  Write formal proofs in natural language and LaTeX.

  Language:Haskell32967

• ariroffe/logics

  Logics is a Python framework for mathematical logic

  Language:Python21402

• mattia-furlan/MasterThesisCTT

  Haskell implementation of a version of cubical type theory developed for my master thesis

  Language:Haskell16101

• diku-dk/sml-parse

  Standard ML Parser Combinator Library

  Language:Standard ML151101

• ioannad/NBG_HOL

  A formalisation of NBG set theory in Isabelle/HOL

  Language:Isabelle6102

• gmilmei/lispkit

  Original LispKit in Pascal ported to Free Pascal

  Language:Pascal4201

• martinberger/hol-c

  A proof-of-concept LCF-style interactive theorem prover for HOL(C)

  Language:Scala4231

• kappelmann/Isabelle-Set

  Soft types for Isabelle - bringing types to the world of set-theory.

  Language:Isabelle3105