samuelgruetter Goto Github PK

agda-summer-school

Summer school on programming in Agda

bedrock2

Towards a low-level systems programming language with a verified compiler

big-bench

Beyond the Imitation Game collaborative benchmark for enormous language models

calculus-of-constructions

a simple implementation of the pure calculus of constructions

certicoq

check-ci-success

Using GitHub's API, check if the CI run on a given branch succeeded

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.

coq-record-update

Library to create Coq record update functions

coq-smt-notations

A quick hack to ask any SMT solver if your Coq goal is true

coq-tricks

Collection of Useful Features of the Coq Proof Assistant

counterexamples

What's the best way to find counterexamples to Coq conjectures?

courseracodesamplesreactiveprogramming

critbit-coq

(An attempt at) A formally verified Coq implementation of crit-bit trees

dafny

Dafny is a verification-aware programming language

dafny-wiki

dafnytour

dot

formalization of the Dependent Object Types (DOT) calculus

dot-calculus

Formalization of the Dependent Object Types (DOT) calculus

dotfiles

Configuration files

dotty

Research platform for new language concepts and compiler technologies for Scala.

egg

egg is a flexible, high-performance e-graph library

exfalsopp

exfalso++ is an improved version of Coq's exfalso tactic

fiat-crypto

Cryptographic Primitive Code Generation by Fiat

frap

Formal Reasoning About Programs

fsm

Finite State Machine Designer

hireslofps

Sharing a high-resolution but low framerate image stream

homepage

My homepage/blog

icfpcontest2015

ICFP Programming Contest 2015 Submission

interactiontrees

Formalization of the Interaction Tree Datatype in Coq

isa_formal_spec_public_review

Locus site for Public Review of Several RISC-V ISA Formal Specs