Commit graph

Select branches

Hide pull requests

main

Mono Color

• 355d09145d
  
  improve directory structure main Michael Sippel 2024-09-29 22:52:59 +0200
• 54b9d4c06d
  
  coq: add preliminary preservation proof Michael Sippel 2024-09-24 12:08:16 +0200
• d31101103f
  
  coq: add expr_fv_type Michael Sippel 2024-09-24 12:08:00 +0200
• d050baf88d
  
  improve ladder-type example Michael Sippel 2024-09-24 12:07:13 +0200
• 04cc471c19
  
  remove related work slide Michael Sippel 2024-09-24 11:57:47 +0200
• ab81edb753
  
  add bib file Michael Sippel 2024-09-24 11:57:34 +0200
• 69176aef2b
  
  add summary & traits/wrappers Michael Sippel 2024-09-24 11:56:08 +0200
• 251289c510 subtype graphs as backup slides Michael Sippel 2024-09-24 10:36:55 +0200
• 3adeebc8eb add image for morphism condition Michael Sippel 2024-09-24 10:28:14 +0200
• 7f45198cd1 intro slide Michael Sippel 2024-09-24 10:10:25 +0200
• e0f467c848 add inversion lemmas (without proof) Michael Sippel 2024-09-24 05:32:59 +0200
• 666d14e91d add #[export] to all Hints Michael Sippel 2024-09-24 08:49:20 +0200
• 63b121a815
  
  add inversion lemmas (without proof) Michael Sippel 2024-09-24 05:32:59 +0200
• 48429c6316
  
  add preliminary proof of transl_preservation (with env_wf Γ admitted) Michael Sippel 2024-09-24 04:57:16 +0200
• ac63139c67 add preconditions of expr_lc in eval; use coinductive quantification in T_TypeAbs Michael Sippel 2024-09-24 04:28:41 +0200
• ae9e451bf3 work on slides Michael Sippel 2024-09-23 23:06:05 +0200
• 10cd2f9bc9 fix expr_open & expr_lc for let case Michael Sippel 2024-09-22 17:34:12 +0200
• f0d9a550b6 prove typing preservation of morphism translation Michael Sippel 2024-09-22 15:57:15 +0200
• 236d6d9c09 add env_wf Michael Sippel 2024-09-22 15:52:06 +0200
• 3d200e141e add expr_open_lc and expr_subst_open lemmas Michael Sippel 2024-09-22 13:37:49 +0200
• 080aa0ffec use 'binds' instead of 'In' for environments Michael Sippel 2024-09-22 13:37:11 +0200
• 4fde2442f1 fix naming of rules in expr_lc Michael Sippel 2024-09-22 13:36:20 +0200
• a5d8cb979b rename context to env Michael Sippel 2024-09-21 17:26:26 +0200
• cc96cee283
  
  add environment library to metatheory Michael Sippel 2024-09-21 17:22:49 +0200
• d690d6dcdc
  
  organize coq sources in subdirectories Michael Sippel 2024-09-21 13:00:57 +0200
• 30fe571a39
  
  open scopes locally Michael Sippel 2024-09-21 12:33:10 +0200
• 6f3b0fbc0b
  
  typing: use cofinite quantification Michael Sippel 2024-09-21 06:48:26 +0200
• 67e4c13d57
  
  translate morphism path: fix morph mapping Michael Sippel 2024-09-21 06:47:55 +0200
• 3c86dde677
  
  improve notation for opening/substitution & add proof for expr_subst_fresh Michael Sippel 2024-09-21 01:43:25 +0200
• 4b76d6a982
  
  improve type-opening lemmas Michael Sippel 2024-09-21 01:05:28 +0200
• f8effc45ad add evaluation for debruijn terms Michael Sippel 2024-09-21 00:36:50 +0200
• 8b19caa9f2 add substitution & opening fixpoints for expressions Michael Sippel 2024-09-21 00:34:06 +0200
• 3c5859b43c add translate_typing for debruijn terms Michael Sippel 2024-09-20 22:04:19 +0200
• 1edbb8d748 add context, morphism translation & typing for debruijn terms Michael Sippel 2024-09-20 21:41:38 +0200
• f76cec4a9d add subtype relations for debruijn terms Michael Sippel 2024-09-20 20:39:43 +0200
• 377f57e124 equiv_debruijn: add more hints & simplify TEq_Symm proof Michael Sippel 2024-09-20 20:35:29 +0200
• 1d6fb9ab6d add equivalence relation for debruijn types Michael Sippel 2024-09-20 20:30:32 +0200
• f174eb1061 add notation for debruijn terms Michael Sippel 2024-09-20 19:53:27 +0200
• c4f4e56fee move subst/opening lemmas to separate file Michael Sippel 2024-09-20 19:41:27 +0200
• b97cb84caf use 'atom' in debruijn terms & complete proofs about type subst / open Michael Sippel 2024-09-20 19:23:22 +0200
• 9264d28837 take over Metatheory, FiniteSet & Atom libraries from popl-tutorial Michael Sippel 2024-09-19 21:15:43 +0200
• bd3504614b
  
  popl-tutorial Fsub: sanitize base libraries Michael Sippel 2024-09-19 21:13:59 +0200
• 6773f81ff5
  
  initial beamer Michael Sippel 2024-09-19 14:17:48 +0200
• fd2c035902
  
  work on soundness proofs & fix bug in translate_typing Michael Sippel 2024-09-19 07:01:31 +0200
• dbfe0cf4de
  
  add initial impl of debruijn terms Michael Sippel 2024-09-19 01:48:12 +0200
• 826077e37b
  
  coq: add translate_typing example Michael Sippel 2024-09-19 01:46:29 +0200
• d23ad61ba3
  
  coq: type equiv: add subfun/submorph Michael Sippel 2024-09-19 01:41:51 +0200
• 6e5c832db7
  
  add notation for sequence types & use notations everywhere Michael Sippel 2024-09-18 11:15:20 +0200
• 633843d9c7
  
  work on abstract & intro Michael Sippel 2024-09-17 18:36:38 +0200
• 127debf945
  
  terms notation: add ident rule to allow variables in notation instance Michael Sippel 2024-09-17 03:14:49 +0200
• f53f226f55
  
  remove module wraps in each file Michael Sippel 2024-09-17 03:13:36 +0200
• 05c137c489
  
  import implementation of Fsub from the Coq tutorial of UPenn Michael Sippel 2024-09-16 17:58:18 +0200
• 44d8d401d8
  
  adapt eval relation & add reduction example add expr_descend Notation [{ e des τ }] Michael Sippel 2024-09-16 17:54:24 +0200
• 12da3e97bd
  
  change meaning of expr_ascend to only explicitly state the top segment of the type ladder. Michael Sippel 2024-09-16 15:58:29 +0200
• cae0572e1b
  
  wip on preservation proof Michael Sippel 2024-09-16 15:14:53 +0200
• 638ddf4fd1
  
  coq: add translate_typing Michael Sippel 2024-09-08 15:34:15 +0200
• 10ca08c5a0
  
  coq typing relation: add DescendImplicit rule in addition to Descend rule for explicit type-downcasts Michael Sippel 2024-09-08 15:33:54 +0200
• 4b3358372e
  
  coq: typing relation fix ctx assignments in premisse Michael Sippel 2024-09-08 15:32:54 +0200
• b44e443879
  
  add translate_morphism_path \& morphism path examples Michael Sippel 2024-09-08 15:30:09 +0200
• 850285cff0
  
  morphism paths: add Lift path Michael Sippel 2024-09-08 15:29:47 +0200
• 865ceff7d4
  
  add remaining notations for expr_term Michael Sippel 2024-09-08 15:28:44 +0200
• c3d1649402
  
  expr term: remove explicit variable-type from expr_let Michael Sippel 2024-09-08 14:48:36 +0200
• bf7846294f
  
  coq: move context into separate module, define morphism-path & redefine typing rules Michael Sippel 2024-09-05 12:47:30 +0200
• e62c028126
  
  paper: adapt soundness theorems Michael Sippel 2024-09-05 12:46:24 +0200
• 6f81686105
  
  paper: define morphism-path relation, redefine typing-relation \& translation Michael Sippel 2024-09-05 11:20:21 +0200
• 2d557e51e4
  
  WIP coq: debruijn terms Michael Sippel 2024-09-04 12:47:03 +0200
• d1742c51d5
  
  coq: remove delta_step definition Michael Sippel 2024-09-04 12:46:37 +0200
• 1bd55cd8c3
  
  paper: rename inference rules to match coq definitions Michael Sippel 2024-09-04 12:45:33 +0200
• fd8ca35a27
  
  paper: add new coq files to appendix Michael Sippel 2024-09-04 12:44:24 +0200
• b31c8abc6c
  
  initial definition of soundness theorems Michael Sippel 2024-09-04 12:41:17 +0200
• 2db774ae68
  
  initial definition of expand_morphisms Michael Sippel 2024-09-04 12:41:00 +0200
• 75fab989d7
  
  work on typing rules Michael Sippel 2024-09-04 12:39:15 +0200
• b978637b57
  
  coq: change notation brackets for terms Michael Sippel 2024-08-22 09:57:47 +0200
• 719cb8ec4a
  
  coq: add value requirement in E-App2 Michael Sippel 2024-08-22 09:57:05 +0200
• 9c17e9e642
  
  paper: rename inference rules to match coq definitions Michael Sippel 2024-08-22 09:05:20 +0200
• 4323e7d09f
  
  coq: add another typing example Michael Sippel 2024-08-22 08:31:14 +0200
• ad107759bf
  
  coq: expr alpha conversion Michael Sippel 2024-08-22 08:30:46 +0200
• 39f312b401
  
  coq: rename expr_term constructors: remove 'tm' prefix Michael Sippel 2024-08-22 01:04:40 +0200
• 61f1234fcc
  
  coq: add 'compatible' typing relation Michael Sippel 2024-08-21 20:04:20 +0200
• 361d03c117
  
  coq: reimplement type substitution and alpha conversion in types Michael Sippel 2024-08-21 20:03:46 +0200
• 0caf3ff514
  
  coq: remove type_unit & type_num Michael Sippel 2024-08-21 16:10:15 +0200
• 42ae93f2d7
  
  coq: add subtype relations Michael Sippel 2024-08-21 15:02:43 +0200
• a65a33d9d6
  
  coq: rename type equality rules to have prefix TEq_ Michael Sippel 2024-08-18 11:24:37 +0200
• d08144434c
  
  complete type distribute/condense definitions Michael Sippel 2024-08-18 10:56:06 +0200
• 221c017640
  
  coq: alpha conversion in types Michael Sippel 2024-08-18 10:47:35 +0200
• 3a84dada65
  
  coq notation definition for expressions Michael Sippel 2024-08-18 10:27:21 +0200
• 8da65e4d38
  
  coercion semantics Michael Sippel 2024-08-08 13:20:18 +0200
• b8e8543813
  
  paper: subtype relation Michael Sippel 2024-08-08 13:19:17 +0200
• 06dba1f348
  
  paper: add type equivalence Michael Sippel 2024-08-08 13:18:36 +0200
• 35e0a9b62b
  
  paper:work on syntax definition & substitutions Michael Sippel 2024-08-08 13:17:34 +0200
• 3f27afa253
  
  paper: simplify pseudo grammar Michael Sippel 2024-08-07 16:00:01 +0200
• f135a5ed43
  
  paper: add appendix with coq listings Michael Sippel 2024-08-07 15:59:03 +0200
• c7794d8a89
  
  paper: wip add more lemmas Michael Sippel 2024-07-27 13:30:34 +0200
• eebb096f8a
  
  coq: wip typing Michael Sippel 2024-07-27 13:30:12 +0200
• d880e07d57
  
  coq: notations for type terms Michael Sippel 2024-07-27 13:28:52 +0200
• 13165a7951
  
  coq: smallstep: define delta expansion Michael Sippel 2024-07-25 12:42:32 +0200
• ec955c3c19
  
  coq: add morphism type Michael Sippel 2024-07-25 12:41:44 +0200
• 292234c247
  
  rename term types to expr_term and type_term and type_abs->type_univ, type_app->type_spec Michael Sippel 2024-07-25 11:04:56 +0200
• ec1a2ab4a4
  
  add initial main.tex Michael Sippel 2024-07-24 11:23:51 +0200
• 84ad8d9897 coq: add some examples of bb-encoding Michael Sippel 2024-07-24 11:20:43 +0200