Skip to content

Certifier: add html agda docs to metatheory documentation #7819

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
basetunnel wants to merge 1 commit into
base: master
Choose a base branch
from
+18 −0
Open

Certifier: add html agda docs to metatheory documentation #7819

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 18 additions & 0 deletions plutus-metatheory/src/index.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,13 @@ untyped version of PLC which can also be executed directly.
The final two pieces are a type checker which is guaranteed to be
sound and an executable that is intended to be compiled into Haskell.

A separate family of modules specify UPLC compiler optimizations as syntactic
binary relations. The relations are (semi-)decidable, so for a given pair of
input/output terms, we can produce a proof when the pass behaved according to
specification. This is the basis of the `--certify` flag available in the Plinth
compiler and UPLC CLI tool. The Plinth user guide contains more detail on how to
use the certifier.

1. [Types](#types)
2. [Normalisation of types](#normal-types)
3. [Builtin machinery](#builtins)
Expand All @@ -41,6 +48,7 @@ sound and an executable that is intended to be compiled into Haskell.
7. [Untyped terms](#untyped-terms)
8. [A typechecker](#type-checker)
9. [An executable](#executable)
10. [Certified compilation](#certified-compilation)

## Types

Expand Down Expand Up @@ -200,3 +208,13 @@ to produce an executable.
import Main
```


## Certified Compilation

The top-level module that defines the `certify` function, imports all
translation relations and their (semi-)decision procedures.

```
import VerifiedCompilation
```

Loading