Two experimental implementations of fragments of purely linear logic, extended with temporal and ergometric types as well as constraints over natural numbers in Presburger arithmetic and termination checking.
- Parallel Complexity Analysis with Temporal Session Types
- Work Analysis with Resource-Aware Session Types
- Session Types with Arithmetic Refinements and Their Application to Work Analysis
- Circular Proofs as Session-Typed Processes: A Local Validity Condition
Authors:
- Ankush Das
- Farzaneh Derakhshan
- Frank Pfenning
For details on the two implementations see the subdirectories:
The implementation language for both is Standard ML.