| --------------------+------------------------------------------ | |
| Utils.agda | General utility functions |
| Param.agda | Parametricity-specific utilities |
| Label.agda | General definition of the Label structure |
| --------------------+------------------------------------------ | |
| Booleans.agda | Example in Paper: Booleans |
| BooleansWrong.agda | Example in Paper: Booleans, bad case |
| LIO.agda | Example in Paper: LIO implementation |
| LIOProof.agda | Example in Paper: LIO proof |
| MultefSimple.agda | Example in Paper: Multef |
| FIOSimple.agda | Example in Paper: Effects |
| --------------------+------------------------------------------ |
-
Notifications
You must be signed in to change notification settings - Fork 0
MaximilianAlgehed/DynamicIFCTheoremsForFree
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
Using parametricity to prove noninterference for LIO and Faceted Values
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published