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 169
    • Issues 169
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 24
    • Merge requests 24
  • 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
  • Issues
  • #329
Closed
Open
Issue created Jun 25, 2020 by Ralf Jung@jungOwner

Iris Website Reform

We had a long discussion on Mattermost today discussing potential improvements to the website. Some of the take-aways include:

  • We'd like to move to a static site generator (Jekyll, or something else if someone makes a good pitch).
  • We'd like to split the website into sub-pages, as the list of papers is getting too long.
  • We'd like to have the website repo public for contributors. I think it would make sense to have it in the Iris organization here on MPI's GitLab.
  • In terms of content, the concern that triggered this discussion was along the lines of "(some) people think Iris is just for academic/toy/ML-like languages". We should probably put the fact that Iris is very flexible front and center, maybe by picking a few papers to display on the front page that use Iris for various models of real-world definitely-not-toy languages (RustBelt for Rust, runST for Haskell, DOT for Scala, "Non-Determinism in C Expressions" for C, Goose for Go, and once that paper exists RefinedC for C).
  • We could also highlight the different kinds of properties people verify in Iris (type system soundness, refinement, verification of concurrent algorithms, non-interference, ...).

I expect I will take the lead on setting up the infrastructure for wiring up GitLab with Jekyll and GH pages, and @robbertkrebbers offered to take the lead on the content side of things.

Assignee
Assign to
Time tracking