Pinned Repositories
ActorModel
Simple visualizer for Actor model
CCLV
Fenestra6502
A 6502 system for high-level programming languages
Finesse
Tiny Scheme implementation
Geta
Simple proof checker for equational logic
Guedra
Concurrent GUI toolkit for OCaml
Guedra-draw
Draw widget for Guedra
ocaml-csp
CSP library for OCaml
plancklisp
Lisp interpreter in x86 assembler language for Linux
SyncStitch
A Refinement Checker based on CSP
hatsugai's Repositories
hatsugai/Fenestra6502
A 6502 system for high-level programming languages
hatsugai/SyncStitch
A Refinement Checker based on CSP
hatsugai/ocaml-csp
CSP library for OCaml
hatsugai/CCLV
hatsugai/Geta
Simple proof checker for equational logic
hatsugai/Guedra
Concurrent GUI toolkit for OCaml
hatsugai/ActorModel
Simple visualizer for Actor model
hatsugai/Guedra-draw
Draw widget for Guedra
hatsugai/plancklisp
Lisp interpreter in x86 assembler language for Linux
hatsugai/Finesse
Tiny Scheme implementation
hatsugai/CSP-semantics
hatsugai/Correctness-Model-Checking
Proof of correctness of CTL model checking algorithm
hatsugai/Correctness-of-BFS
Proof of correctness of breadth-first-search with Isabelle/HOL
hatsugai/CSP-Prover
hatsugai/Dual6502
hatsugai/process_model
hatsugai/simulation_traces
Formal proof by Isabelle/HOL: Existence of asymmetric weak simulation between a deterministic transition system and a nondeterministic transition system implies the inclusion of traces.