RetroFed Forums
Your home away from modern life.
Search Categories Forum list Register Log in
About RetroFed
RetroFed

Welcome to the nostalgia-filled piefed instance of yesteryear.

Open Registration with Application questionnaire.

If you have a question or comment you can post in !meta@retrofed.com or message @DosDude@retrofed.com or @Die4Ever@retrofed.com

In case of downtime and/or emergency, we will post updates on @DosDude@mastodon.social

Some rules we try to uphold:

  • Be civil. Bigotry is not welcome. This includes (but is not limited to): transphobia, queerphobia, racism, ageism and ableism. We do not promote hate.
  • Communities need to be Retro or Retro-adjacent.
  • Please don't upload pornographic content. (use an external image host for that)
72 registered users
Administrators: DosDude, Die4Ever
Visit retrofed.com
Formal Methods !formal_methods@programming.dev
Moderators: Ategon, synthetic_apriori
New Topic RetroFed Forums Forum Index » Formal Methods
 Topics  Replies  Author  Score  Last Post 
No new posts The changing role of finite-state model checking (ahelwer.ca) 0 lysdexic 4 »
No new posts My first verified (imperative) program [Lean] (markushimmel.de) 0 armchair_progamer 1 »
No new posts Verified Effectful Programming in F* - Catalin Hritcu (www.youtube.com) 0 cyph3rPunk 1 »
No new posts Linearizability! Refinement! Prophecy! (proving code correctness) (surfingcomplexity.blog) 0 armchair_progamer 1 »
No new posts The Hitchhiker’s Guide to Logical Verification (book) (browncs1951x.github.io) 0 armchair_progamer 2 »
No new posts A curated list of awesome Rust checkers (burtonqin.github.io) 0 armchair_progamer 1 »
No new posts Modeling B-trees in TLA+ (surfingcomplexity.blog) 0 armchair_progamer 1 »
No new posts Nondeterminism in Formal Specification (buttondown.email) 0 armchair_progamer 1 »
No new posts Diffusion On Syntax Trees For Program Synthesis (tree-diffusion.github.io) 0 armchair_progamer 1 »
No new posts Some notes on Rust, mutable aliasing and formal verification (graydon2.dreamwidth.org) 0 armchair_progamer 1 »
No new posts coq-of-rust: convert Rust programs into Coq definitions to formally reason about them (github.com) 0 armchair_progamer 1 »
No new posts Agda Core: The Dream and the Reality (jesper.cx) 0 armchair_progamer 1 »
No new posts Dafny Power User: Type-parameter modes: variance and cardinality preservation (leino.science) 0 armchair_progamer 1 »
No new posts Verus: Verified Rust for low-level systems code (github.com) 0 armchair_progamer 1 »
No new posts Narya: A proof assistant for higher-dimensional type theory (GitHub) (github.com) 0 armchair_progamer 1 »
No new posts Don't let Alloy facts make your specs a fiction (www.hillelwayne.com) 0 armchair_progamer 1 »
No new posts I formally modeled Dreidel for no good reason (buttondown.email) 0 armchair_progamer 1 »
No new posts TLA+ in Isabelle/HOL (davecturner.github.io) 0 armchair_progamer 1 »
No new posts rzk: an experimental proof assistant for synthetic ∞-categories (rzk-lang.github.io) 0 armchair_progamer 1 »
No new posts Lean/Coq/Isabel and Their Proof Trees (lakesare.brick.do) 0 armchair_progamer 1 »
No new posts So you want to be a proof engineer? (proofcraft.org) 0 synthetic_apriori 1 »
No new posts #239 Grigore Rosu: The K framework - a framework to formally define all programming languages (www.youtube.com) 0 demesisx 1 »
No new posts The Dafny Programming and Verification Language (dafny.org) 0 synthetic_apriori 1 »
No new posts Back in June, NASEM hosted a workshop on using AI for mathematical reasoning; many talks discussed the use of AI in developing formal mathematical proofs and formally verifying software (www.nationalacademies.org) 0 synthetic_apriori 1 »
No new posts category-theory: An axiom-free formalization of category theory in Coq for personal study and practical work by John Wiegley (github.com) 0 demesisx 1 »
New Topic Page 1   Next
Powered by RetroFed · PieBB frontend · All times are Europe/Amsterdam