Global ETD Search
Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.
Results
Showing 1 to 11 of 11 for “"Isabelle/HOL"”.
-
Towards justifying computer algebra algorithms in Isabelle/HOL
… thesis describes an ongoing effort using the Isabelle theorem prover to certify the cylindrical algebraic decomposition (CAD) algorithm, which has been widely implemented to solve non-linear problems in various engineering and mathematical fields. Because of the sophistication of this …
-
Formalising Combinatorial Structures and Proof Techniques in Isabelle/HOL
… for combinatorics using the proof assistant Isabelle/HOL. These, in turn, explore the interplay between different mathematical fields in a formal environment. The thesis begins with an outline of the locale-centric approach for formalising complex hierarchies, inspired by Ballarin and further …
-
Formalisation and execution of Linear Algebra: theorems and algorithms
… and execution of Linear Algebra algorithms in Isabelle/HOL, an interactive theorem prover. The work is based on the HOL Multivariate Analysis library, whose matrix representation has been refined to datatypes that admit a representation in functional programming languages. This enables the …
-
Reasoning Using Higher-Order Abstract Syntax in a Higher-Order Logic Proof Environment: Improvements to Hybrid and a Case Study
… Hybrid system, a formal theory implemented in Isabelle/HOL to support specifying and reasoning about formal systems using higher-order abstract syntax (HOAS). We modify Hybrid's type of terms, which is built definitionally in terms of de Bruijn indices, to exclude at the type level terms with …
-
A general theory of syntax with bindings
… at the same time we give a formalization, in the Isabelle/HOL proof assistant. Our theory uses explicit names for variables, and then deals with alpha-equivalence classes, remaining intuitive and close to informal mathematics, although being fully formalized and sound in classical high-order …
-
Qualitative Spatial Reasoning With Super-Intuitionistic Logics
… has been developed, by formalising them in Isabelle-HOL, an interactive theorem-prover based on classical higher-order logic. A partial decidability result is given for an extension of intuitionistic second-order propositional logics, together with an account of its mechanisation.
-
Theorem-proving distributed algorithms with dynamic analysis
… a new model for specifying I/O automata in the Isabelle theorem prover's logic, and prove the soundness of a technique for verifying invariants in this model in the Isabelle prover. We develop methods for generating proofs of I/0 automata for two theorem provers, the Larch Prover and …
-
Forward with separation logic
… of the above, in the interactive proof assistant Isabelle/HOL, and enable automation with several interactive proof tactics.
-
Mechanising and evolving the formal semantics of WebAssembly: the Web's new low-level language
… mechanising the WebAssembly formal semantics in Isabelle/HOL while it was being drafted, I discovered a number of errors in the specification, drove the adoption of official corrections, and provided the first type soundness proof for the corrected language. This thesis also details a verified …
-
Formally verifying the security properties of a proof-of-stake blockchain protocol
… In this project, we attempt to formalise, in Isabelle/HOL, the combinatorial analysis used to prove that Ouroboros satisfies common prefix with near certainty. We cover the case of a static stake protocol under a few assumptions: the network is synchronous, the majority of the stake is honest, …
-
A mechanized Theory of Aspects
… mechanized in the interactive theorem prover Isabelle/HOL. The emphasis of the work is placed on two different fields. Fundamental questions of modularity, type soundness and subtyping form the first such field. Technical considerations such as binders, variable representation and code …