Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 14
    • Merge requests 14
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !564

Add a verified interpreter for HeapLang

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Tej Chajed requested to merge tchajed/iris-coq:interpreter into master Nov 03, 2020
  • Overview 43
  • Commits 11
  • Pipelines 0
  • Changes 7

The code in this file is pretty different from most of Iris, using a lot more automation and Ltac. If and when we are happy with the overall idea of merging an interpreter then we can figure out the naming and code style issues I'm sure this file has.

Much credit for the interpreter and proof strategy goes to Sydney Gibson, who wrote an interpreter for GooseLang that I basically back-ported to HeapLang.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: interpreter