tchajed/seplogic-demo

Stars
4
Rank 3,304,323 (Top 66 %)
Language Coq
License
MIT License
Created about 4 years ago
Updated about 1 year ago

tchajed/seplogic-demo

tchajed

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

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

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

coq-ltac2-experiments

All the code I've ever written in Ltac2

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

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