tchajed/coq-ltac2-experiments

Stars
11
Rank 1,694,829 (Top 34 %)
Language Coq
Created almost 5 years ago
Updated almost 4 years ago

tchajed/coq-ltac2-experiments

tchajed

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

All the code I've ever written in Ltac2

minimal-elf

Creating a minimal ELF file

iris-simp-lang

We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.

coq-record-update

Library to create Coq record update functions

ltac2-tutorial

coq-tla

rdb

Debugger written in Rust

coq-tactical

Library of Coq proof automation

database-stream-processing-theory

Formalization of DBSP

audiobook-splitting

Splitting audiobooks by chapter

coq-io

Modeling I/O in Coq using free monads

div-regex

Computing regular expressions to test divisibility

goedel-t

Formalization of termination of Gödel's System T

rust-nbd

Network Block Device (NBD) server and client written in Rust

protocol-verification-fa2023

Assignments for COMP SCI 839 from UW-Madison in Fall 2023

futex-tutorial

coq-sep-logic

Separation logic library for Coq

Voting.jl

Implementations of several voting schemes in Julia

personal-website-demo

Template for a statically generated academic website

regex-derivative

Regex derivatives in Coq

iris-named-props

Named Props for Iris

portmap

Map domain names to local ports with DNS and reverse proxy magic

ivy-mutex

Mutex proof in Ivy

coq-array

Coq library for array indexing and subslicing

mailboat

Verified mail server

seplogic-demo

Demos for lecture on Separation Logic by O'Hearn from CACM 2019.

dafny-syntax-tutorial

Short introduction to Dafny

botc-tools

Storyteller tools for Blood on the Clocktower

coq-curry-howard

What a Coq proof actually is

coq-project-template

Example project setup for Coq that supports git submodule dependencies

dotfiles

Personal dotfiles configuration

coq-transitions

Coq library for writing transition relations

coq-survey

Proposed questions for a Coq user survey

coq-record-update-plugin

cardinality

Reasoning about finite type cardinality in Coq

strong-induction

Proof of strong induction in Coq

sys-verif-fa24-proofs

Assignment repo for Systems Verification Fall 2024 at UW-Madison

coq-classes

A library of typeclasses for Coq

ivy-to-mypyvy

Convert an Ivy liveness problem to a mypyvy input file

madcap

A music clustering program.

specious-db

Simple persistent key-value store for prototyping a verified version

r2048-ai

AI for the 2048 game

wordenc

web-timer

Simple web timer

coq-tactic-timing

heedless-db

Simple, persistent key-value store implemented in Haskell to prototype a verified version

go-awol

Go write-ahead logging

iris-bank-demo

Demo of using Iris to prove a simple property of a concurrent program

games-night

Rules for board games we play often

100game

Analysis of the 100 game

detex-abstract

Turn a LaTeX abstract into a Markdown abstract

coq-arrows-theorem

Proof of Arrow's Impossibility Theorem

entropic-poetry

Encoding data using poetry

verus-vstd-models