A mechanized proof of soundness of calculus defined in A Theory of Quoted Code Patterns which is a formalization of pattern matching on code available in Scala 3 as part of its new macro system.
-
Updated
Jul 23, 2020 - TeX
A mechanized proof of soundness of calculus defined in A Theory of Quoted Code Patterns which is a formalization of pattern matching on code available in Scala 3 as part of its new macro system.
Aiming to have a personal well-founded math library written in lean. Hope it works...
Mechanized formalization of Implicit resolution in Agda
Homeworks for 'formal languages and grammars' discipline
Categorical Semantics of Intuitionistic Multiplicative Linear Logic written in Isabelle/HOL
Equivalent definitions of flatness
first-order logic and set theory
Coq Formalisation of "A Fine-Grained Evaluation Strategy for Delimited-Control Operators shift0/dollar"
Formal Verification of Telegram's MTProto 2.0
Linear algebra formalization in Agda
Formalization of Robin Milner's bigraphs in Isabelle/HOL
Repository hosting resources for the 2024 workshop "Computer-Verified Proofs: 48 Hours in Rome" organised by @oliver-butterley, @RafaelGreenblatt and @marcolenci.
The stages that Blue Husky Studios goes throguh when creating a product
A formalization of SRPs and Control Plane Compression in Coq.
A Coq formalisation of the R programming language
Calculating the Risk of Valve Failures when Maintaining Water Supply Networks
An unusual construction of the real numbers using Isabelle/HOL
Repository hosting resources for the 2024 workshop "Lean for the Curious Mathematician".
Formalisation of Selinger proof about quantum gate
Add a description, image, and links to the formalization topic page so that developers can more easily learn about it.
To associate your repository with the formalization topic, visit your repo's landing page and select "manage topics."