Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
I
Iris
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package Registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Service Desk
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Matthieu Sozeau
Iris
Commits
8bfd3d5aeb45b995ae7f101569c239759a40b992
Select Git revision
Branches
20
coq-13969
master
default
protected
ralf/tc-weakestpre
ci/ralf/Z_of_nat
hai/si_embed
hai/si_experiment
ci/ralf/bi-language
ralf/coq-bug-13942
iris-3.4
ci/janno/strict-tc-resolution
ralf/vs-mask-adjust
ralf/make_laterable
ci/robbert/into_fupd
ci/robbert/frame_fractional
robbert/fupd_elim
ci/robbert/coq_bug_7773
ci/robbert/mapsto_persist
step_fupdN_support
ci/debug
ralf/wp_apply-no-simpl
Tags
13
iris-3.4.0
iris-3.3.0
iris-3.2.0
iris-3.1.0
iris-3.0.0
iris-2.0
iris-2.0-rc2
iris-2.0-rc1
iris-1.1
iris-1.0
hope-2015-coq-1
appendix-1.0.0
appendix-1
33 results
iris
docs
Author
Search by author
Any Author
authors
0 authors
Mar 15, 2016
update bibs
· 8bfd3d5a
Ralf Jung
authored
9 years ago
8bfd3d5a
copy some intuition from the paper
· a331d9fa
Ralf Jung
authored
9 years ago
a331d9fa
more consistent naming
· 2fc7c984
Ralf Jung
authored
9 years ago
2fc7c984
docs: reference Lars' metric space paper
· 3b8b2aec
Ralf Jung
authored
9 years ago
3b8b2aec
Mar 14, 2016
typo fix
· af0d3b95
Ralf Jung
authored
9 years ago
af0d3b95
some more intuition for SProp
· 6b839469
Ralf Jung
authored
9 years ago
6b839469
Mar 12, 2016
docs: atomic(...) consistent with Coq
· 04d3ee68
Ralf Jung
authored
9 years ago
04d3ee68
docs: typos, nits
· 0816b3de
Ralf Jung
authored
9 years ago
0816b3de
docs: complete model description
· 7cb94e3e
Ralf Jung
authored
9 years ago
7cb94e3e
docs: describe the part of the model that works for any UPred
· 82aee390
Ralf Jung
authored
9 years ago
82aee390
change some lfiting lemmas to make it clear why they are called 'atomic'
· 7c354ddb
Ralf Jung
authored
9 years ago
7c354ddb
docs: derived lifting rules
· 0dbb9032
Ralf Jung
authored
9 years ago
0dbb9032
docs: define RAs
· a072e355
Ralf Jung
authored
9 years ago
a072e355
docs: various nits
· 610698ec
Ralf Jung
authored
9 years ago
610698ec
Mar 11, 2016
docs: UPred
· 94042bb7
Ralf Jung
authored
9 years ago
94042bb7
docs: type-level later
· 3d79ec6c
Ralf Jung
authored
9 years ago
3d79ec6c
docs: explain why agreement has a chain
· 979bd7af
Ralf Jung
authored
9 years ago
979bd7af
docs: global ghost functor
· 6562c4be
Ralf Jung
authored
9 years ago
6562c4be
docs: complete invariant namespaces
· 2af215bf
Ralf Jung
authored
9 years ago
2af215bf
start describing invariant namespaces
· 23c152d5
Ralf Jung
authored
9 years ago
23c152d5
docs: one-shot
· 0876cbad
Ralf Jung
authored
9 years ago
0876cbad
docs: update iris.sty, some more on agreement
· 11069713
Ralf Jung
authored
9 years ago
11069713
docs: locally non-expansive/contractive also applies to bifunctors
· 9ac461b1
Ralf Jung
authored
9 years ago
9ac461b1
docs: get rid of division :)
· d6dba217
Ralf Jung
authored
9 years ago
d6dba217
docs: record notation
· 60a13f4a
Ralf Jung
authored
9 years ago
60a13f4a
docs: align CMRA inclusion notation with Coq
· 12447782
Ralf Jung
authored
9 years ago
12447782
assume we can get rid of division for the paper
· 978eec47
Ralf Jung
authored
9 years ago
978eec47
Mar 10, 2016
docs: minor editing
· 5c9a1a55
Ralf Jung
authored
9 years ago
5c9a1a55
rant about division...
· d72200d0
Ralf Jung
authored
9 years ago
d72200d0
Mar 09, 2016
docs: notation for nonexp functions
· cd3a1805
Ralf Jung
authored
9 years ago
cd3a1805
docs: update iris.sty
· d7cae999
Ralf Jung
authored
9 years ago
d7cae999
docs: define agreement
· 21ad2d96
Ralf Jung
authored
9 years ago
21ad2d96
different style for mval
· f9a1045e
Ralf Jung
authored
9 years ago
f9a1045e
consistent letter for COFEs
· b592424f
Ralf Jung
authored
9 years ago
b592424f
Mar 08, 2016
docs: actually having some start symbol for wpre makes it way more readable
· 5f230a8e
Ralf Jung
authored
9 years ago
5f230a8e
docs: safety adequacy
· 27dfd62d
Ralf Jung
authored
9 years ago
27dfd62d
docs: change wpre order of arguments to match how they are displayed
· b56508ff
Ralf Jung
authored
9 years ago
b56508ff
docs: lifting axioms
· b0386f85
Ralf Jung
authored
9 years ago
b0386f85
add bidirectional turnstile
· 662d20dc
Ralf Jung
authored
9 years ago
662d20dc
give some derived proof rules
· 3cf0a5fc
Ralf Jung
authored
9 years ago
3cf0a5fc
Loading