Skip to content

ShrohanMohapatra/ExplorePLT

BranchesTags

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

48 Commits
ReferenceMaterials
ReferenceMaterials
 
 
HomotopyTypeTheory.pdf
HomotopyTypeTheory.pdf
 
 
churchNumerals.py
churchNumerals.py
 
 
cykAlgo.py
cykAlgo.py
 
 
earleyAlgo.py
earleyAlgo.py
 
 
earleyAlgo1.py
earleyAlgo1.py
 
 
example1.txt
example1.txt
 
 
example2.txt
example2.txt
 
 
example3.txt
example3.txt
 
 
factorial.dfy
factorial.dfy
 
 
factorial.dll
factorial.dll
 
 
factorial.dll.mdb
factorial.dll.mdb
 
 
fibonacci.dfy
fibonacci.dfy
 
 
fibonacci.dll
fibonacci.dll
 
 
fibonacci.dll.mdb
fibonacci.dll.mdb
 
 
firstRefresh.dfy
firstRefresh.dfy
 
 
firstRefresh.dll
firstRefresh.dll
 
 
firstRefresh.dll.mdb
firstRefresh.dll.mdb
 
 
inversemod.dfy
inversemod.dfy
 
 
lambdaCalc1.py
lambdaCalc1.py
 
 
lambdaCalculusTools.txt
lambdaCalculusTools.txt
 
 
lambdaTM1.txt
lambdaTM1.txt
 
 
lambdaTutorial1.py
lambdaTutorial1.py
 
 
lambdaTutorial2.py
lambdaTutorial2.py
 
 
lambdaTutorial3.py
lambdaTutorial3.py
 
 
larkTutorial1.py
larkTutorial1.py
 
 
larkTutorial2.py
larkTutorial2.py
 
 
lexerEarly.txt
lexerEarly.txt
 
 
loopInvariant.nb
loopInvariant.nb
 
 
pell.dfy
pell.dfy
 
 
powerExp.dfy
powerExp.dfy
 
 
powerExp.dll
powerExp.dll
 
 
powerExp.dll.mdb
powerExp.dll.mdb
 
 
turingMachine1.py
turingMachine1.py
 
 
typeTheory.pdf
typeTheory.pdf
 
 

About

A repository that describes my explorations on formal verification using Dafny, techniques from programming language theory such as CYK parsing, Earley parsing, type-theoretic things like lambda calculus etc.

Topics

lambda-calculus lambda-expressions dafny earley-algorithm formal-verification earley-parser turing-completeness formal-specification loop-invariants weakest-preconditions cyk-algorithm church-thesis
Activity

Stars

4 stars

Watchers

1 watching

Forks

1 fork
Report repository

Releases

No releases published

Packages

 
 
 

Contributors

Languages