Skip to content
GitLab
Explore
Sign in
Amin Timany
iris-coq
Repository
Branches
Overview
Active
Stale
All
less_canonical
5226baf6
·
FAIL : Less canonical projections.
·
Feb 22, 2016
primitive_sealing
e7ff4737
·
Use primitive records for sealing.
·
Feb 25, 2016
ralf/magic-singleton
9bd5532f
·
demonstrate a weird issue
·
Mar 02, 2016
jh_coreless_cmras
9780d3ef
·
WIP
·
May 17, 2016
jh_partial_core
a12e05c2
·
WIP
·
May 22, 2016
jh_inductive_pairs
7d2a0390
·
Failed attempt at improving performances of pairs by using inductives
·
Jun 16, 2016
rename
d44399bb
·
Rename rvs -> shift, iVs -> iShift, iVsIntro -> iShiftIntro.
·
Aug 11, 2016
janno/early-scopes
a0067662
·
Define E and V scopes in program_logic
·
Aug 25, 2016
janno/hoare-notation
d0fd0444
·
Turn iProp into a notation.
·
Aug 29, 2016
clairvoyant
4acdc774
·
Add clairvoyant_coin example
·
Jun 20, 2019
iris/iris!266
erasure_backup
913ddab8
·
move lemmas out of erasure
·
Nov 01, 2019
lang_lemmas
d2d19975
·
Apply suggestion to theories/program_logic/ectx_language.v
·
Nov 06, 2019
iris/iris!324
erasure-squashed
34383242
·
Prove erasure of prophecy variables in heap_lang
·
Nov 21, 2019
erasure
a466a842
·
Prove erasure of prophecy variables in heap_lang
·
Nov 21, 2019
iris/iris!275
monotone
be38c833
·
Apply 1 suggestion(s) to 1 file(s)
·
May 07, 2021
iris/iris!597
master
default
6839ae86
·
Merge branch 'ralf/paradox' into 'master'
·
Sep 08, 2023
iris/iris!11
mra-changelog
b9aea5e1
·
Add my name
·
Sep 09, 2023