|
|
f76cec4a9d
|
add subtype relations for debruijn terms
|
2024-09-21 00:41:45 +02:00 |
|
|
|
377f57e124
|
equiv_debruijn: add more hints & simplify TEq_Symm proof
|
2024-09-21 00:41:45 +02:00 |
|
|
|
1d6fb9ab6d
|
add equivalence relation for debruijn types
|
2024-09-21 00:41:45 +02:00 |
|
|
|
f174eb1061
|
add notation for debruijn terms
|
2024-09-21 00:41:45 +02:00 |
|
|
|
c4f4e56fee
|
move subst/opening lemmas to separate file
|
2024-09-21 00:41:45 +02:00 |
|
|
|
b97cb84caf
|
use 'atom' in debruijn terms & complete proofs about type subst / open
|
2024-09-21 00:41:45 +02:00 |
|
|
|
9264d28837
|
take over Metatheory, FiniteSet & Atom libraries from popl-tutorial
|
2024-09-21 00:41:40 +02:00 |
|
|
|
bd3504614b
|
popl-tutorial Fsub: sanitize base libraries
mostly add Admitted everywhere
|
2024-09-19 21:13:59 +02:00 |
|
|
|
6773f81ff5
|
initial beamer
|
2024-09-19 14:17:48 +02:00 |
|
|
|
fd2c035902
|
work on soundness proofs & fix bug in translate_typing
|
2024-09-19 07:02:27 +02:00 |
|
|
|
dbfe0cf4de
|
add initial impl of debruijn terms
|
2024-09-19 01:48:12 +02:00 |
|
|
|
826077e37b
|
coq: add translate_typing example
& other minor stuff
|
2024-09-19 01:46:29 +02:00 |
|
|
|
d23ad61ba3
|
coq: type equiv: add subfun/submorph
|
2024-09-19 01:41:51 +02:00 |
|
|
|
6e5c832db7
|
add notation for sequence types & use notations everywhere
|
2024-09-18 11:15:20 +02:00 |
|
|
|
633843d9c7
|
work on abstract & intro
|
2024-09-17 18:36:38 +02:00 |
|
|
|
127debf945
|
terms notation: add ident rule to allow variables in notation instance
|
2024-09-17 03:14:49 +02:00 |
|
|
|
f53f226f55
|
remove module wraps in each file
|
2024-09-17 03:13:36 +02:00 |
|
|
|
05c137c489
|
import implementation of Fsub from the Coq tutorial of UPenn
taken from 'https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/index.html'
|
2024-09-16 17:58:18 +02:00 |
|
|
|
44d8d401d8
|
adapt eval relation & add reduction example
add expr_descend Notation [{ e des τ }]
|
2024-09-16 17:54:32 +02:00 |
|
|
|
12da3e97bd
|
change meaning of expr_ascend to only explicitly state the top segment of the type ladder.
also add associativity of ladder types in type-equivalence
|
2024-09-16 15:58:29 +02:00 |
|
|
|
cae0572e1b
|
wip on preservation proof
|
2024-09-16 15:14:53 +02:00 |
|
|
|
638ddf4fd1
|
coq: add translate_typing
|
2024-09-08 15:34:15 +02:00 |
|
|
|
10ca08c5a0
|
coq typing relation: add DescendImplicit rule in addition to Descend rule for explicit type-downcasts
add one more typing example
|
2024-09-08 15:33:54 +02:00 |
|
|
|
4b3358372e
|
coq: typing relation fix ctx assignments in premisse
|
2024-09-08 15:32:54 +02:00 |
|
|
|
b44e443879
|
add translate_morphism_path \& morphism path examples
|
2024-09-08 15:30:09 +02:00 |
|
|
|
850285cff0
|
morphism paths: add Lift path
|
2024-09-08 15:29:47 +02:00 |
|
|
|
865ceff7d4
|
add remaining notations for expr_term
|
2024-09-08 15:28:44 +02:00 |
|
|
|
c3d1649402
|
expr term: remove explicit variable-type from expr_let
|
2024-09-08 14:48:36 +02:00 |
|
|
|
bf7846294f
|
coq: move context into separate module, define morphism-path & redefine typing rules
|
2024-09-05 12:47:30 +02:00 |
|
|
|
e62c028126
|
paper: adapt soundness theorems
|
2024-09-05 12:46:24 +02:00 |
|
|
|
6f81686105
|
paper: define morphism-path relation, redefine typing-relation \& translation
|
2024-09-05 11:20:21 +02:00 |
|
|
|
2d557e51e4
|
WIP coq: debruijn terms
|
2024-09-04 12:47:03 +02:00 |
|
|
|
d1742c51d5
|
coq: remove delta_step definition
|
2024-09-04 12:46:37 +02:00 |
|
|
|
1bd55cd8c3
|
paper: rename inference rules to match coq definitions
|
2024-09-04 12:45:33 +02:00 |
|
|
|
fd8ca35a27
|
paper: add new coq files to appendix
|
2024-09-04 12:44:24 +02:00 |
|
|
|
b31c8abc6c
|
initial definition of soundness theorems
|
2024-09-04 12:41:17 +02:00 |
|
|
|
2db774ae68
|
initial definition of expand_morphisms
|
2024-09-04 12:41:00 +02:00 |
|
|
|
75fab989d7
|
work on typing rules
|
2024-09-04 12:39:15 +02:00 |
|
|
|
b978637b57
|
coq: change notation brackets for terms
|
2024-08-22 09:57:47 +02:00 |
|
|
|
719cb8ec4a
|
coq: add value requirement in E-App2
|
2024-08-22 09:57:05 +02:00 |
|
|
|
9c17e9e642
|
paper: rename inference rules to match coq definitions
|
2024-08-22 09:05:20 +02:00 |
|
|
|
4323e7d09f
|
coq: add another typing example
|
2024-08-22 08:31:14 +02:00 |
|
|
|
ad107759bf
|
coq: expr alpha conversion
|
2024-08-22 08:30:46 +02:00 |
|
|
|
39f312b401
|
coq: rename expr_term constructors: remove 'tm' prefix
|
2024-08-22 08:19:48 +02:00 |
|
|
|
61f1234fcc
|
coq: add 'compatible' typing relation
|
2024-08-21 20:04:20 +02:00 |
|
|
|
361d03c117
|
coq: reimplement type substitution and alpha conversion in types
|
2024-08-21 20:03:46 +02:00 |
|
|
|
0caf3ff514
|
coq: remove type_unit & type_num
|
2024-08-21 16:10:15 +02:00 |
|
|
|
42ae93f2d7
|
coq: add subtype relations
|
2024-08-21 15:02:43 +02:00 |
|
|
|
a65a33d9d6
|
coq: rename type equality rules to have prefix TEq_
|
2024-08-18 11:24:37 +02:00 |
|
|
|
d08144434c
|
complete type distribute/condense definitions
|
2024-08-18 10:56:06 +02:00 |
|
