Name		Name	Last commit message	Last commit date
CIC1.lean		CIC1.lean
CIC2.lean		CIC2.lean
CIC3.lean		CIC3.lean
README.md		README.md
agediff.hs		agediff.hs
code01.dfy		code01.dfy
code01.lean		code01.lean
code01.ml		code01.ml
code01.v		code01.v
code01_compiler.dfy		code01_compiler.dfy
code01_simplified.dfy		code01_simplified.dfy
code01_simplified.lean		code01_simplified.lean
code01_simplified_buggy.dfy		code01_simplified_buggy.dfy
code01_simplified_compiler.dfy		code01_simplified_compiler.dfy
code01_simplified_compiler_calc.dfy		code01_simplified_compiler_calc.dfy
code02.v		code02.v
code03.v		code03.v
code04.v		code04.v
code05.v		code05.v
code09.ml		code09.ml
code09.rkt		code09.rkt
code10.ml		code10.ml
code10.rkt		code10.rkt
code10.scm		code10.scm
code13.ml		code13.ml
code15.lhs		code15.lhs
code16.pl		code16.pl
code20.elf		code20.elf
code20.v		code20.v
eg1.rs		eg1.rs
eg2.rs		eg2.rs
eg3.rs		eg3.rs
eg4.rs		eg4.rs
eg5.rs		eg5.rs
eg_verus_pcell.rs		eg_verus_pcell.rs
ex1.go		ex1.go
ex2.go		ex2.go
ex3.go		ex3.go
factorial.c		factorial.c
factorial.dfy		factorial.dfy
factorial2.dfy		factorial2.dfy
graph.png		graph.png
hoare.c		hoare.c
hoare.dfy		hoare.dfy
io.hs		io.hs
iris_installation.md		iris_installation.md
kowalski.png		kowalski.png
lean-toolchain		lean-toolchain
lecture.hs		lecture.hs
logic_programming.ipynb		logic_programming.ipynb
lst.hs		lst.hs
m.hs		m.hs
ownership.v		ownership.v
separation_logic.v		separation_logic.v
state.hs		state.hs
sum.dfy		sum.dfy
walk.hs		walk.hs

Repository files navigation

Code from CS152 lectures

14 stars

4 watching