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 148
    • Issues 148
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 9
    • Merge requests 9
  • 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
  • Issues
  • #2

Closed
Open
Created Oct 24, 2015 by Ralf Jung@jungOwner

Bring back the Bind rule

Once #1 (closed) is done: Provide a module ectx_lang for languages with an evaluation context interface, and show that this implies a bind rule. This will be similar to how core_lang looks right now, but not identical - in particular, the user will be in control of fork.

@swasey I recall you changed the core_lang axioms some time ago to actually make some sense. These changed axioms will then become part of ectx_lang. Are they suitably canonical, or is there something we should discuss there? Do we know that an actual Coq implementation of some lambda calculus can satisfy these axioms? Once we have ectx_lang in the development, how much work would it take to port your old AutoSubst-based language to that interface, so that we have a (nice?) example of an instantiated language?

Assignee
Assign to
Time tracking