Skip to content

GitLab

  • Menu
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 153
    • Issues 153
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 8
    • Merge requests 8
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • 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
  • 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
Reviewer
Request review from
Time tracking
Source branch: interpreter