forked from AndrasKovacs/stlc-nbe
-
Notifications
You must be signed in to change notification settings - Fork 0
akaposi/stlc-nbe
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
module Readme where
{-
Full correctness proof of normalization-by-evaluation for simply typed
lambda calculus.
We use function extensionality and Axiom K, but no other postulates,
holes or unsafe pragmas. Also, the use of Axiom K could be eliminated with
a moderate amount of work.
-}
-- Order in which you probably want to view modules
------------------------------------------------------------
import Syntax
import Renaming
import Nf
import Substitution
import Conversion
import Normalization
import Stability
4A51
import Completeness
import Soundness
-- Main results
------------------------------------------------------------
open import Lib
open Syntax
open Nf
open Conversion
nf : ∀ {Γ A} → Tm Γ A → Nf Γ A
nf = Normalization.nf
stability : ∀ {Γ A}(n : Nf Γ A) → nf ⌜ n ⌝ ≡ n
stability = Stability.stab
soundness : ∀ {Γ A}{t t' : Tm Γ A} → t ~ t' → nf t ≡ nf t'
soundness = Soundness.sound
completeness : ∀ {Γ A}(t : Tm Γ A) → t ~ ⌜ nf t ⌝
completeness = Completeness.complete
About
Correctness proof for normalization-by-evaluation for STLC
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published
Languages
- Agda 100.0%