CakeML: A Verified Implementation of ML
-
Updated
Oct 15, 2026 - Standard ML
#
formal-semantics
Here are 49 public repositories matching this topic...
Tableau-based Theorem Prover for Natural Logic and Language
natural-language-processing formal-semantics prolog theorem-proving natural-language-inference theorem-prover nli semantic-tableau natural-logic natural-tableau lambda-logical-form
-
Updated
Sep 9, 2026 - Prolog
Formal semantics of LLVM IR in K
-
Updated
Jun 25, 2015 - LLVM
⚛ React-tRace is a React Hooks interpreter and a visualizer based on a formal semantics
-
Updated
Jun 5, 2026 - OCaml
A retargetable and extensible synthesis-based compiler for modern hardware architectures
dsl high-performance llvm formal-semantics program-synthesis halide compilers vectorization formal-verification compiler-construction mlir isa-semantics retargetability instruction-selection automlir
-
Updated
Nov 20, 2025 - LLVM
Formal Semantics of P4 in K
interpreter formal-semantics verification symbolic-execution model-checking p4language p4 translation-validation
-
Updated
May 21, 2021 - P4
Distributional Formal Semantics (DFS) tools
-
Updated
Oct 17, 2022 - Prolog
A style guide for Coq
c haskell dependent-types style-guide ocaml coq proof formal-semantics verification proof-assistant software-engineering formal-methods formal-verification formal-mathematics formal-specification formal-proofs appliedfm
-
Updated
Nov 30, 2021
A library for manipulating DMRS structures
python nlp mrs natural-language-processing delph-in hpsg semantics natural-language formal-semantics dependency-graph linguistics computational-linguistics dmrs minimal-recursion-semantics
-
Updated
Mar 3, 2021 - Python
Practical Program Analysis (academic course) presented in Innopolis University in 2023
-
Updated
Oct 13, 2026 - TeX
C++L is C++ with Laws: an ambiguity-free, proof-carrying superset C++ based language in which humans or AIs can specify intent as machine-checkable Laws, implementations are accepted only when those Laws are proven, and all proof machinery erases to ordinary optimized C++ compiled by Clang/LLVM.
programming-language compiler cpp llvm formal-semantics theorem-proving clang language-design formal-methods program-verification cpp20 format-verification
-
Updated
Oct 9, 2026 - C++
Untyped Lambda Calculus interpreter performing alpha-conversion, capture-avoiding substitution, and normal-order beta reduction with 0 pip.
lambda-calculus formal-semantics beta-reduction programming-language-theory agentic-ai genpark-skill
-
Updated
Sep 9, 2026 - Python
Untyped Lambda Calculus interpreter performing alpha-conversion, capture-avoiding substitution, and normal-order beta reduction with 0 pip.
lambda-calculus formal-semantics beta-reduction programming-language-theory agentic-ai genpark-skill
-
Updated
Sep 9, 2026 - Python
Formal specification of a pure, functional subset of Python for scientific computing
python programming-language functional-programming formal-semantics interoperability scientific-computing language-design language-specification operational-semantics pure-functional
-
Updated
Oct 14, 2026 - TeX
Formally correct DSLs
haskell dsl formal-semantics dissertation metacompiler domain-specific-language formal-verification metalanguage
-
Updated
Jun 5, 2017 - Haskell
Clojure implementation of Generalized Quantifiers for English sentences.
-
Updated
Oct 26, 2013 - Clojure
fspl: Formal Semantics of Programming Languages
-
Updated
Feb 12, 2020
Add this topic to your repo
To associate your repository with the formal-semantics topic, visit your repo's landing page and select "manage topics."