Commit Graph

15 Commits

Author SHA1 Message Date
JanUlrich
21328a3d05 Unify 2024-04-03 15:54:08 +02:00
Andreas Stadelmeier
87f413241a Add ANF transformation. Define LetFJ. Change Constraint generation. Cleanup old explanation of Capture conversion. Add example to Constraint generation 2024-03-30 00:07:26 +01:00
Andreas Stadelmeier
7b86dc0cf3 Add ANF transformation. Change syntax of TamedFJ. Restructure Unify description. Some fixes in Unify 2024-03-28 03:40:39 +01:00
Andreas Stadelmeier
e93a762441 Add Wildcard Environment to intro Unify example 2024-03-27 01:53:23 +01:00
JanUlrich
e7b6786f08 Add Syntax and type rules for a normal form 2024-03-15 17:37:58 +01:00
Andreas Stadelmeier
c7212cd7c6 Introduce new challenge (principal type). Restructure and remove some parts. 2024-03-13 00:30:16 +01:00
Andreas Stadelmeier
5055364de5 Add Recap in introduction 2024-03-07 03:32:56 +01:00
Andreas Stadelmeier
4547fbab40 add shuffle example to wildcard introduction 2024-03-06 00:33:54 +01:00
Andreas Stadelmeier
e15d61cdae Add Global Type Inference introduction 2024-03-05 17:12:56 +01:00
Andreas Stadelmeier
fca93d7ec6 Introduce normal type placeholders \ntv 2024-02-12 15:28:44 +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
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
ab5f9d0f73 Describe tph helper function 2023-12-27 19:03:25 +01:00
Andreas Stadelmeier
8f3d49d70f Initial commit. Applying LipICS style to wildcard paper 2023-12-27 14:29:33 +01:00