Pinned Repositories
cakeml
CakeML: A Verified Implementation of ML
FPBench
A standard for floating point accuracy benchmarks
Dandelion
A verified certificate checker for elementary functions
HOL4-Snippets
Collection of handy yasnippet scripts to ease writing HOL4 files
HOL4-Tutorial
A tutorial for the HOL4 theorem prover using Lassie.
Lassie
A tactic language framework to ease proving theorems in HOL4.
Prog2-Eclipse-Demo
Dieses Repository enthält ein Projekt, an dem die Benutzung von Eclipse vorgeführt werden soll.
HOL
Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
HeikoBecker's Repositories
HeikoBecker/Dandelion
A verified certificate checker for elementary functions
HeikoBecker/HOL4-Tutorial
A tutorial for the HOL4 theorem prover using Lassie.
HeikoBecker/Prog2-Eclipse-Demo
Dieses Repository enthält ein Projekt, an dem die Benutzung von Eclipse vorgeführt werden soll.
HeikoBecker/HOL4-Snippets
Collection of handy yasnippet scripts to ease writing HOL4 files
HeikoBecker/Lassie
A tactic language framework to ease proving theorems in HOL4.
HeikoBecker/awesome-config
My Awesome WM configuration files
HeikoBecker/cakeml
CakeML: A Verified Implementation of ML
HeikoBecker/cc2013
Compiler written during the lecture compiler construction at the Universität des Saarlandes by Fabian Kosmale, Patrick Klitzke and me (Heiko Becker)
HeikoBecker/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
HeikoBecker/daisy
HeikoBecker/DNSummer2015
Pushing bits and bytes through pipes
HeikoBecker/FPBench
Working toward a standard of floating point accuracy benchmarks.
HeikoBecker/GalaxyMerchant
HeikoBecker/HeikoBecker.github.io
GitHub Pages Website
HeikoBecker/HOL
Canonical sources for HOL4 theorem-proving system. Branch `develop` is where “mainline development” occurs; when `develop` passes our regression tests, `master` is merged forward to catch up.
HeikoBecker/hol-guidebook
HOL Guidebook
HeikoBecker/opam-repository
Main public package repository for OPAM, the source package manager of OCaml.
HeikoBecker/org-zk
Use org-mode as an emacs frontend for implementing a "Zettelkasten"
HeikoBecker/TheoremProving-Notes
Notes and tactic collections for theorem provers I have used