senvas

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-21 13:12:11 +02:00

d690d6dcdc organize coq sources in subdirectories

30fe571a39 open scopes locally

Compare 2 commits »

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-21 06:48:30 +02:00

6f3b0fbc0b typing: use cofinite quantification

67e4c13d57 translate morphism path: fix morph mapping

Compare 2 commits »

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-21 01:43:54 +02:00

3c86dde677 improve notation for opening/substitution & add proof for expr_subst_fresh

4b76d6a982 improve type-opening lemmas

Compare 2 commits »

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-21 00:42:05 +02:00

f8effc45ad add evaluation for debruijn terms

8b19caa9f2 add substitution & opening fixpoints for expressions

3c5859b43c add translate_typing for debruijn terms

1edbb8d748 add context, morphism translation & typing for debruijn terms

f76cec4a9d add subtype relations for debruijn terms

Compare 11 commits »

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-20 22:04:16 +02:00

874633681a add translate_typing for debruijn terms

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-20 21:41:57 +02:00

29a2edf4be add context, morphism translation & typing for debruijn terms

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-20 20:39:39 +02:00

cf7a265d17 add subtype relations for debruijn terms

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-20 20:35:24 +02:00

0da2ff2afb equiv_debruijn: add more hints & simplify TEq_Symm proof

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-20 20:30:37 +02:00

c5a4626551 add equivalence relation for debruijn types

d22ae9a682 add notation for debruijn terms

7a6ed28c0a move subst/opening lemmas to separate file

Compare 3 commits »

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-20 19:25:32 +02:00

cafa9808aa add Metatheory.v to _CoqProject

2ae7297da5 use 'atom' in debruijn terms & complete proofs about type subst / open

Compare 2 commits »

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-19 21:15:45 +02:00

b9314c345d take over FiniteSet & Atom libraries from popl-tutorial

bd3504614b popl-tutorial Fsub: sanitize base libraries

Compare 2 commits »

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-19 14:18:04 +02:00

6773f81ff5 initial beamer

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-19 07:02:47 +02:00

fd2c035902 work on soundness proofs & fix bug in translate_typing

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-19 01:48:49 +02:00

dbfe0cf4de add initial impl of debruijn terms

826077e37b coq: add translate_typing example

d23ad61ba3 coq: type equiv: add subfun/submorph

6e5c832db7 add notation for sequence types & use notations everywhere

Compare 4 commits »

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-17 18:36:37 +02:00

633843d9c7 work on abstract & intro

127debf945 terms notation: add ident rule to allow variables in notation instance

f53f226f55 remove module wraps in each file

Compare 3 commits »

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-16 17:58:25 +02:00

05c137c489 import implementation of Fsub from the Coq tutorial of UPenn

senvas pushed to main at syntaxAlchemist/ladder-calculus

2024-09-16 17:54:54 +02:00

44d8d401d8 adapt eval relation & add reduction example

12da3e97bd change meaning of expr_ascend to only explicitly state the top segment of the type ladder.

cae0572e1b wip on preservation proof

Compare 3 commits »

senvas deleted branch master from syntaxAlchemist/ladder-calculus

2024-09-08 15:37:22 +02:00

senvas deleted branch wip from syntaxAlchemist/ladder-calculus

2024-09-08 15:37:19 +02:00

senvas created branch main in syntaxAlchemist/ladder-calculus

2024-09-08 15:36:24 +02:00