- ILSyntax.v defines syntax of the payoff expressions language (PEL)
- ILSemantics.v semantics of the PEL
- ILTranslation.v defines compilation from the financial contracts DSL to PEL. Includes proof of compilation soundness
- CutPayoff.v defines the cutPayoff transformation, which allows to parametarize the compiled code with "current time" parameter. Manipulation this parameter one recover evolution of the contract over time in the form of payoff expression. Also contains proofs of soundness wrt. contract reduction semantics.
- CutPayoffN.v a generalization of theorems about cutPayoff soundness for n-step case.
- Days.v defines functions allowing to extract information about transaction dates and dates of observable values (like stocks prices),which contract depends on. Could be used for reindexing transformation for array representation of the external environment.
Payoff
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|
parent directory.. | ||||