Andreas Stadelmeier
|
a151415950
|
SameW rule soundness
|
2024-04-03 00:45:51 +02:00 |
|
Andreas Stadelmeier
|
9556f1521e
|
Cleanup. Define mutual subtyping as equality
|
2024-03-26 15:41:48 +01:00 |
|
Andreas Stadelmeier
|
e40693a7de
|
Remove comments (cleanup). Add Clear and Exclude rules. Change Unify Soundness premise
|
2024-03-25 19:12:35 +01:00 |
|
Andreas Stadelmeier
|
f2002ea833
|
Add GenDelta for WTVS. Restructure step 2. Comment out old version
|
2024-03-25 14:09:46 +01:00 |
|
Andreas Stadelmeier
|
4eb7b1ce19
|
🛠 work in progress
|
2024-03-04 15:37:21 +01:00 |
|
Andreas Stadelmeier
|
56b2cddf18
|
🛠 work in progress sync 🛠
|
2024-02-28 17:51:41 +01:00 |
|
Andreas Stadelmeier
|
c880503ba5
|
Work in Progress
|
2024-02-14 01:56:35 +01:00 |
|
Andreas Stadelmeier
|
5074c21943
|
Cleanup
|
2024-02-11 23:30:09 +01:00 |
|
Andreas Stadelmeier
|
10fcfcfea0
|
Cleanup Introduction. Fix method environment in Type Rules
|
2024-02-07 18:26:41 +01:00 |
|
Andreas Stadelmeier
|
26678767c2
|
Cleanup, rephrase introduction. Fix and Cleanup type rules. Remove override
|
2024-02-07 17:29:41 +01:00 |
|
Andreas Stadelmeier
|
f40299a36c
|
hange Equals rule. Add explanations
|
2024-02-06 18:05:05 +01:00 |
|
Andreas Stadelmeier
|
43e75127b3
|
Nearly finish soundness for TYPE
|
2024-02-05 14:54:42 +01:00 |
|
Andreas Stadelmeier
|
3d10421439
|
Remove adopt. Add Gen-X to Unify
|
2024-02-02 19:23:00 +01:00 |
|
JanUlrich
|
743e32daa9
|
Use Unify recursive in method call soundness proof
|
2024-02-01 18:17:46 +01:00 |
|
Andreas Stadelmeier
|
edc7f87108
|
Type Soundness
|
2024-02-01 14:54:44 +01:00 |
|
Andreas Stadelmeier
|
3716fcdfd1
|
Type soundness
|
2024-01-31 18:06:04 +01:00 |
|
Andreas Stadelmeier
|
8e3707b9a6
|
WF lemma
|
2024-01-31 07:51:17 +01:00 |
|
Andreas Stadelmeier
|
54fb6f9f0f
|
Fix Unify WF lemma
|
2024-01-30 23:03:34 +01:00 |
|
Andreas Stadelmeier
|
319f080a8d
|
Add LessdotCC REmove to unify. Fix Soundness lemma
|
2024-01-30 16:19:01 +01:00 |
|
JanUlrich
|
9aa89933ce
|
Add WF type environment lemma (work in progress)
|
2024-01-29 18:44:21 +01:00 |
|
JanUlrich
|
95d0d00339
|
Fix WF-Class, WF-Var and Type for method call
|
2024-01-29 18:39:18 +01:00 |
|
Andreas Stadelmeier
|
6494394db6
|
Comments on Well-Formedness proof
|
2024-01-29 13:41:12 +01:00 |
|
Andreas Stadelmeier
|
0101341841
|
Fix and comment
|
2024-01-26 16:50:56 +01:00 |
|
JanUlrich
|
ba4b78b57b
|
Soundness method call
|
2024-01-24 13:18:48 +01:00 |
|
Andreas Stadelmeier
|
05b6b84e1e
|
Cleanup soundness. Add Delta environment to Unify input
|
2024-01-23 16:30:24 +01:00 |
|
Andreas Stadelmeier
|
881eecef8a
|
Add <._c constraint to Type for field and alter soundness proof
|
2024-01-23 00:34:48 +01:00 |
|
Andreas Stadelmeier
|
b775045d17
|
Soundness for Prepare and Capture
|
2024-01-22 15:34:33 +01:00 |
|
Andreas Stadelmeier
|
e3a393520d
|
fix capture soundness proof
|
2024-01-22 01:03:58 +01:00 |
|
Andreas Stadelmeier
|
5578415ed3
|
Fix Capture Soundness
|
2024-01-17 12:53:36 +01:00 |
|
Andreas Stadelmeier
|
8907cac94a
|
Prepare Soundness
|
2024-01-17 10:58:16 +01:00 |
|
Andreas Stadelmeier
|
bc4fcaf43c
|
Change Prepare rule to simpler version
|
2024-01-16 18:03:54 +01:00 |
|
JanUlrich
|
521dee7fa2
|
Soundness Prepare
|
2024-01-16 10:00:47 +01:00 |
|
Andreas Stadelmeier
|
b546da831d
|
Start soundness for prepare rule
|
2024-01-15 20:43:19 +01:00 |
|
Andreas Stadelmeier
|
bf401f1f08
|
Add prepare rule
|
2024-01-10 16:03:23 +01:00 |
|
Andreas Stadelmeier
|
93c0b76b9c
|
Add <:_? constraint (work in progress)
|
2024-01-09 16:28:19 +01:00 |
|
Andreas Stadelmeier
|
e6807e65fc
|
Start with Type soundness for method call
|
2024-01-09 07:33:17 +01:00 |
|
Andreas Stadelmeier
|
3a499d2e6d
|
Add well-formedness description
|
2024-01-04 01:33:36 +01:00 |
|
Andreas Stadelmeier
|
d4c43c04a7
|
Add to Soundness. Start Wellformed lemma, add T-Rules
|
2023-12-31 03:32:26 +01:00 |
|
Andreas Stadelmeier
|
14ebe4c360
|
Fix errrors in TYPE. Fix Unify soundness proof. start TYPE Soundness proof. Add elimination/transformation WildFJ <-> WildFJ-GT
|
2023-12-29 03:38:07 +01:00 |
|
Andreas Stadelmeier
|
18dd2325a6
|
Start TYPE soundness
|
2023-12-27 23:05:34 +01:00 |
|
Andreas Stadelmeier
|
8f3d49d70f
|
Initial commit. Applying LipICS style to wildcard paper
|
2023-12-27 14:29:33 +01:00 |
|