Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • masters/rusthornbelt protected
  • masters/weak_mem protected
  • ci/ike/frame_exist
  • ralf/prop-level-wand
  • msammler/new-contractive
  • xldenis/pldi-submission
  • xldenis/smallvec-push
  • refmut_sync
  • robbert/sprop
  • ci/pinning
  • xldenis/option
  • robbert/Z_of_nat
  • xldenis/type-sum
  • yusuke/tlist_for_prophecy
  • msammler/rustverify_talk
  • gpirlea/pin_semantic
  • rusthornbelt
  • ci/janno/strict-tc-resolution
  • step_indexing_controlled_by_ghosts
  • RBrlx-POPL20-artifact
  • popl18
  • popl18-aec
23 results
Compare
user avatar
Change the sharing view shift to frame a token
Ralf Jung authored 
This also needs changes in type and continuation context inclusion.
It allows us to prove that the empty sum is equal to the empty type.
I also took the opportunity to rename TCtx_holds to TCtx_hasty, which at least says what is "holding".
acddfae5
History
user avatar acddfae5
History
Name Last commit Last update
build
theories
.gitignore
.gitlab-ci.yml
.gitmodules
Makefile
README.md
_CoqProject
opam
opam.pins
README.md

LAMBDA-RUST COQ DEVELOPMENT

This is the Coq formalization of lambda-Rust.

Prerequisites

This version is known to compile with:

  • Coq 8.5pl3
  • Ssreflect 1.6
  • A development version of Iris

The easiest way to install the correct versions of the dependencies is through opam. Once you got opam set up, just run make build-dep to install the right versions of the dependencies. When the dependencies change (e.g., a newer version of Iris is needed), just run make build-dep again.

Alternatively, you can manually determine the required Iris commit by consulting the opam.pins file.

Building Instructions

Run make to build the full development.

For Developers: How to update the Iris dependency

  • Do the change in Iris, push it.
  • In lambdaRust, change opam.pins to point to the new commit.
  • Run "make build-dep" (in lambdaRust) to install the new version of Iris.
  • You may have to do "make clean" as Coq will likely complain about .vo file mismatches.