Skip to content
Snippets Groups Projects
Commit 5f5dd7bc authored by Yusuke Matsushita's avatar Yusuke Matsushita
Browse files

Add a comment on type_soundness

parent 6fe6a563
No related branches found
No related tags found
No related merge requests found
Pipeline #64121 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/typing/soundness.v
+ 2
− 0
View file @ 5f5dd7bc
...@@ -28,6 +28,8 @@ Section type_soundness. ...@@ -28,6 +28,8 @@ Section type_soundness.
Definition main_transformer : predl_trans'ₛ [] () := (λ post '-[], post ()). Definition main_transformer : predl_trans'ₛ [] () := (λ post '-[], post ()).
(* Intuitively, it says that execution of a closed, semantically well-typed
program, without any special precondition, does not get stuck *)
Theorem type_soundness `{!typePreG Σ} (main : val) σ t : Theorem type_soundness `{!typePreG Σ} (main : val) σ t :
(∀ `{!typeG Σ}, typed_val main main_type main_transformer) → (∀ `{!typeG Σ}, typed_val main main_type main_transformer) →
rtc erased_step ([main [exit_cont]%E], ∅) (t, σ) → rtc erased_step ([main [exit_cont]%E], ∅) (t, σ) →
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment