17 Commits

Author	SHA1	Message	Date
JanUlrich	5718c42e28	Change principal type problem in introduction	2024-04-08 21:45:29 +02:00
JanUlrich	2273acadad	FIx	2024-04-05 12:24:42 +02:00
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