tchajed

Professor at UW-Madison. I write software and prove that it does what it's supposed to.

UW-MadisonMadison, WI

Pinned Repositories

perennial
Verifying concurrent crash-safe systems
Language:Coq136 16 2232
botc-tools
Storyteller tools for Blood on the Clocktower
Language:TypeScript1 2 32
coq-record-update
Library to create Coq record update functions
Language:Coq42 8 2815
coq-tactical
Library of Coq proof automation
Language:Coq15 5 12
coq-tla
Language:Coq16 3 00
coq-tricks
Tricks you wish the Coq manual told you
Language:Coq478 27 1419
goose
Goose converts a small subset of Go to Coq
Language:Go90 13 2911
iris-simp-lang
We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.
Language:Coq44 4 14
ltac2-tutorial
Ltac2 tutorial
Language:Coq39 8 03
minimal-elf
Creating a minimal ELF file
Language:Rust101 3 03

tchajed's Repositories

tchajed/coq-tricks
Tricks you wish the Coq manual told you
Language:Coq478 27 1419
tchajed/goose
Goose converts a small subset of Go to Coq
Language:Go90 13 2911
tchajed/iris-simp-lang
We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.
Language:Coq44 4 14
tchajed/coq-record-update
Library to create Coq record update functions
Language:Coq42 8 2815
tchajed/coq-tla
Language:Coq16 3 00
tchajed/protocol-verification-fa2023
Assignments for COMP SCI 839 from UW-Madison in Fall 2023
Language:Dafny8 2 05
tchajed/rust-nbd
Network Block Device (NBD) server and client written in Rust
Language:Rust7 2 0
tchajed/iris-named-props
Named Props for Iris
Language:Coq5 4 14
tchajed/dafny-syntax-tutorial
Short introduction to Dafny
Language:Dafny4 3 0
tchajed/seplogic-demo
Demos for lecture on Separation Logic by O'Hearn from CACM 2019.
Language:Coq4 4 0
tchajed/dotfiles
Personal dotfiles configuration
Language:Emacs Lisp2 3 0
tchajed/botc-tools
Storyteller tools for Blood on the Clocktower
Language:TypeScript1 2 32
tchajed/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
Language:OCaml1 3 0
tchajed/uw-cs-letterhead
LaTeX class to create letterhead for the Department of Computer Sciences at the University of Wisconsin–Madison
Language:PostScript1
tchajed/verus-vstd-models
Language:Rust1
tchajed/web-timer
Simple web timer
Language:TypeScript1 2 0
tchajed/botc-custom-script-json2pdf
Yet Another Custom Script Generator for Blood on the Clocktower
tchajed/coq-arrows-theorem
Proof of Arrow's Impossibility Theorem
Language:Coq
tchajed/cs537-linux-demos
Language:C
tchajed/cs537-sp24-syllabus
PDF syllabus for CS 537 at UW-madison
Language:Python
tchajed/expressiveness-benchmark
tchajed/homebrew-core
:beers: Core formulae for the Homebrew package manager
Language:Ruby3 0
tchajed/ivy-docker
Language:Shell2 0
tchajed/latex-tricks
Advanced tricks for weird LaTeX behavior
1 0
tchajed/marshal
Marshaling library targeting Goose
Language:Go3 02
tchajed/ostep-code
Code from various chapters in OSTEP (http://www.ostep.org)
Language:C1 0
tchajed/ostep-homework
Language:Python1 0
tchajed/personal-cv
Language:TeX3 0
tchajed/personal-website
Sources to generate personal website
Language:Racket2 0
tchajed/starship
☄🌌️ The minimal, blazing-fast, and infinitely customizable prompt for any shell!