Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language
-
Updated
Aug 25, 2022 - Agda
#
operational-semantics
Here are 24 public repositories matching this topic...
A PLT Redex implementation of Featherweight Java
-
Updated
Oct 8, 2012 - Racket
Developing a type system for a minimal reversible functional language.
functional-programming master-thesis semantics type-theory reversible-programming-language diku operational-semantics type-classes program-transformations linear-logic first-match-policy
-
Updated
Aug 30, 2018 - TeX
A Lazy Desugaring System for Evaluating Programs with Sugars
-
Updated
May 8, 2022 - Racket
Pure Demand Operational Semantics
-
Updated
Apr 17, 2024 - OCaml
Записки по курса ,,Семантика на езиците за програмиране"
-
Updated
Jan 14, 2022 - TeX
Brenner is a calculus for reasoning about task parallelism and barrier synchronization. This calculus distils the semantics of phasers and unifies the synchronisation patterns of various abstractions.
synchronization concurrency formal-verification deadlock-detection operational-semantics parallel-programming
-
Updated
Jan 23, 2018 - Coq
Formalization of Big-Stop Semantics (and small-step and big-step semantics) of PCF in Agda
-
Updated
Dec 3, 2025 - Agda
A simple implementation of the operational semantics of small and big steps in Ruby
-
Updated
Mar 26, 2025 - Ruby
Ph.D dissertation website
formal-methods software-product-lines foda process-algebras operational-semantics denotational-semantics axiomatic-semantics
-
Updated
Jan 22, 2025 - HTML
Dyadic linear+affine type system for compile-time WASM memory safety — no use-after-free, no leaks, region-based allocation. Mechanically proved in Coq (preservation 22 open / 910 closed) and Idris2 (8/9 files %default total).
programming-language rust security compiler coq webassembly wasm systems memory-safety agda type-system formal-verification operational-semantics linear-types rsr palimpsest idris2 affine-types hyperpolymath region-calculus
-
Updated
May 20, 2026 - Rust
HIBOU implements a small-step operational semantics for labelled interaction models as well as a trace and multi-trace analysis algorithm
distributed-systems operational-semantics sequence-diagrams formal-models interaction-models multi-trace-analysis
-
Updated
Jan 5, 2025 - Rust
HIBOU EFM implements a small-step operational semantics for interaction models with data and time as well as a trace and multi-trace analysis algorithm
distributed-systems symbolic-execution operational-semantics sequence-diagrams interaction-models multi-trace-analysis
-
Updated
May 21, 2021 - Rust
Coursework for Software Verification (Ranzato, 2025/26): SOS/denotational semantics proofs, abstract interpretation exercises, and Whyle - a full abstract interpreter for While.
static-analysis software-verification abstract-interpretation operational-semantics denotational-semantics while-language
-
Updated
May 3, 2026 - TeX
A GraphQL-like query language. Preliminary experiments.
-
Updated
Feb 14, 2018 - Coq
Executable operational semantics to prototype programming languages
-
Updated
May 9, 2023 - OCaml
Explore dynamic code analysis in an interpreter for a language that allows on-the-fly customization of syntax rules, small-step operational semantics, and typing. This project facilitates real-time modifications to language interpretation, empowering users to adapt coding experiences according to specific needs.
-
Updated
Aug 24, 2024 - Python
Course notes
language programming-language design programming semantics kcl operational-semantics kings structural-semantics kings-college-london programming-languages-and kcl-class-notes
-
Updated
May 5, 2018
AIΩN Foundations Paper II – WARP Graphs: Canonical State Evolution and Deterministic Worldlines
concurrency provenance category-theory warp confluence research-paper aion operational-semantics graph-rewriting determinism graph-transformation adhesive-categories dpoi double-pushout multiway-systems deterministic-replay aion-foundations warp-graphs event-structures typed-graphs
-
Updated
Dec 15, 2025 - TeX
Improve this page
Add a description, image, and links to the operational-semantics topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the operational-semantics topic, visit your repo's landing page and select "manage topics."