User Portlet
| Discussions |
|---|
| Systems descending from NuPRL are based on a realisability semantics, which uses sets of untyped realisers or programs. They have no fixed rules but allow extensions which are justified by the semantics. Systems like Agda, Lean or Idris are based on... |