SDF Chatter
  • Communities
  • Create Post
  • Create Community
  • heart
    Support Lemmy
  • search
    Search
  • Login
  • Sign Up
haxor@derp.fooMB to Hacker News@derp.fooEnglish · 1 year ago

TLA+ in Isabelle/HOL

davecturner.github.io

external-link
message-square
0
fedilink
  • cross-posted to:
  • formal_methods@programming.dev
5
external-link

TLA+ in Isabelle/HOL

davecturner.github.io

haxor@derp.fooMB to Hacker News@derp.fooEnglish · 1 year ago
message-square
0
fedilink
  • cross-posted to:
  • formal_methods@programming.dev
I’m a fan and long-term user of the Isabelle/HOL proof assistant. More recently I have been studying Lamport’s TLA+ system which is a popular choice for writing specifications of systems. This post is a slightly tidied-up version of some notes about my early experiences of playing with the implementation of TLA within Isabelle/HOL, to record a handful of obstacles I hit and some techniques I found useful.

There is a discussion on Hacker News, but feel free to comment here as well.

alert-triangle
You must log in or register to comment.

Hacker News@derp.foo

hackernews@derp.foo

Subscribe from Remote Instance

You are not logged in. However you can subscribe from another Fediverse account, for example Lemmy or Mastodon. To do this, paste the following into the search field of your instance: !hackernews@derp.foo
lock
Community locked: only moderators can create posts. You can still comment on posts.

This community serves to share top posts on Hacker News with the wider fediverse.

Rules
  1. Keep it legal
  2. Keep it civil and SFW
  3. Keep it safe for members of marginalised groups
Visibility: Public
globe

This community can be federated to other instances and be posted/commented in by their users.

  • 1 user / day
  • 1 user / week
  • 1 user / month
  • 2 users / 6 months
  • 61 local subscribers
  • 3.94K subscribers
  • 18K Posts
  • 10.8K Comments
  • Modlog
  • mods:
  • haxor@derp.foo
  • BE: 0.19.8
  • Modlog
  • Instances
  • Docs
  • Code
  • join-lemmy.org