Tej Chajed (@tchajed)
github

tchajed

Twitter logo Share LinkedIn logo Share Facebook logo Share

Top repositories

1

minimal-elf

Creating a minimal ELF file
Rust
104
star
2

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
47
star
3

coq-record-update

Library to create Coq record update functions
Coq
42
star
4

ltac2-tutorial

Ltac2 tutorial
Coq
39
star
5

coq-tla

Coq
20
star
6

rdb

Debugger written in Rust
Rust
16
star
7

coq-tactical

Library of Coq proof automation
Coq
15
star
8

database-stream-processing-theory

Formalization of DBSP
Lean
12
star
9

coq-ltac2-experiments

All the code I've ever written in Ltac2
Coq
11
star
10

audiobook-splitting

Splitting audiobooks by chapter
Python
10
star
11

coq-io

Modeling I/O in Coq using free monads
Coq
9
star
12

div-regex

Computing regular expressions to test divisibility
Python
9
star
13

goedel-t

Formalization of termination of GΓΆdel's System T
Coq
9
star
14

rust-nbd

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

protocol-verification-fa2023

Assignments for COMP SCI 839 from UW-Madison in Fall 2023
Dafny
8
star
16

futex-tutorial

C
8
star
17

coq-sep-logic

Separation logic library for Coq
Coq
7
star
18

Voting.jl

Implementations of several voting schemes in Julia
Julia
7
star
19

personal-website-demo

Template for a statically generated academic website
JavaScript
7
star
20

regex-derivative

Regex derivatives in Coq
Coq
5
star
21

iris-named-props

Named Props for Iris
Coq
5
star
22

portmap

Map domain names to local ports with DNS and reverse proxy magic
Python
5
star
23

ivy-mutex

Mutex proof in Ivy
Shell
5
star
24

coq-array

Coq library for array indexing and subslicing
Coq
5
star
25

mailboat

Verified mail server
Go
4
star
26

seplogic-demo

Demos for lecture on Separation Logic by O'Hearn from CACM 2019.
Coq
4
star
27

dafny-syntax-tutorial

Short introduction to Dafny
Dafny
4
star
28

botc-tools

Storyteller tools for Blood on the Clocktower
TypeScript
3
star
29

coq-curry-howard

What a Coq proof actually is
Coq
3
star
30

coq-project-template

Example project setup for Coq that supports git submodule dependencies
Python
3
star
31

dotfiles

Personal dotfiles configuration
Emacs Lisp
3
star
32

coq-transitions

Coq library for writing transition relations
Coq
2
star
33

coq-survey

Proposed questions for a Coq user survey
2
star
34

coq-record-update-plugin

Coq
2
star
35

cardinality

Reasoning about finite type cardinality in Coq
Coq
2
star
36

strong-induction

Proof of strong induction in Coq
Coq
2
star
37

sys-verif-fa24-proofs

Assignment repo for Systems Verification Fall 2024 at UW-Madison
Coq
2
star
38

coq-classes

A library of typeclasses for Coq
Coq
2
star
39

ivy-to-mypyvy

Convert an Ivy liveness problem to a mypyvy input file
Rust
1
star
40

madcap

A music clustering program.
Go
1
star
41

specious-db

Simple persistent key-value store for prototyping a verified version
Go
1
star
42

r2048-ai

AI for the 2048 game
Rust
1
star
43

wordenc

Go
1
star
44

web-timer

Simple web timer
TypeScript
1
star
45

coq-tactic-timing

Python
1
star
46

heedless-db

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

go-awol

Go write-ahead logging
Go
1
star
48

iris-bank-demo

Demo of using Iris to prove a simple property of a concurrent program
Coq
1
star
49

games-night

Rules for board games we play often
Julia
1
star
50

100game

Analysis of the 100 game
Coq
1
star
51

detex-abstract

Turn a LaTeX abstract into a Markdown abstract
Python
1
star
52

coq-arrows-theorem

Proof of Arrow's Impossibility Theorem
Coq
1
star
53

entropic-poetry

Encoding data using poetry
Haskell
1
star
54

verus-vstd-models

Rust
1
star