`IMP-` infrastructure - Githubissues

wimmers / poly-reductions

Polynomial-time reductions in Isabelle/HOL

2 stars 13 forks source link

Open maxhaslbeck opened 3 years ago

maxhaslbeck commented 3 years ago

Some way to write specifications for IMP- programs
Reasoning infrastructure (Hoare Logic? sequential composition of programs)
Reasoning on polynomials
ASSUME to have encodings (of IMP- programs (enc :: com => nat",dec :: nat => com`), pairs, ...)