pqnelson

pqnelson's Stars

• mikeshulman/narya

  A proof assistant for higher-dimensional type theory

  Language:OCaml1388

• JoshuaGrams/pep

  A Pint-sized Earley Parser

  Language:HTML344

• 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:OCaml331

• augustss/MicroHs

  Haskell implemented with combinators

  Language:Haskell33420

• diku-dk/sml-parse

  Standard ML Parser Combinator Library

  Language:Standard ML151

• vijithassar/lit

  a little preprocessor for literate programming

  Language:Shell1196

• diku-dk/smlpkg

  Generic package manager for Standard ML libraries and programs

  Language:Standard ML1604

• shwestrick/smlfmt

  A custom parser/auto-formatter for Standard ML

  Language:Standard ML6815

• TiarkRompf/collapsing-towers

  Collapsing Towers of Interpreters

  Language:Coq876

• darius/ichbins

  A tiny self-hosting Lisp-to-C compiler

  Language:C23623

• jart/sectorlisp

  Bootstrapping LISP in a Boot Sector

  Language:C1.3k57

• avikalpg/POPL

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

  Language:Oz4413

• mattia-furlan/MasterThesisCTT

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

  Language:Haskell161

• ariroffe/logics

  Logics is a Python framework for mathematical logic

  Language:Python212

• ioannad/NBG_HOL

  A formalisation of NBG set theory in Isabelle/HOL

  Language:Isabelle62

• kappelmann/Isabelle-Set

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

  Language:Isabelle34

• naproche/naproche

  Write formal proofs in natural language and LaTeX.

  Language:Haskell296

• gmilmei/lispkit

  Original LispKit in Pascal ported to Free Pascal

  Language:Pascal41

• 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:Clojure8810

• coalton-lang/coalton

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

  Language:Common Lisp1.1k70

• digama0/mizar-rs

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

  Language:Rust474

• MizarProject/system

  Language:Pascal357

• martinberger/hol-c

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

  Language:Scala41

• antalsz/hs-to-coq

  Convert Haskell source code to Coq source code

  Language:Coq27927

• chrisdone-archive/duet

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

  Language:Haskell2117

• blynn/compiler

  The adventures of a Haskell compiler

  Language:Haskell20915

• slindley/effect-handlers

  Language:Haskell819

• yallop/effects-bibliography

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

  95180

• ocaml-gospel/cameleer

  A Deductive Verification Tool for OCaml Programs

  Language:OCaml608

• estools/esvalid

  confirm that a SpiderMonkey format AST represents an ECMAScript program

  Language:JavaScript267