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 12 of 12 for “"OCaml"”.
-
A static semantics for labels in OCaml
… and a type inferencer for the label-feature of OCaml. Labels in OCaml allow the naming of arguments to functions and are intended to document the code. We provide a type system that describes whether a derived type for an OCaml expression containing labels is correct or not, a type inference …
-
On Reducing the Trusted Computing Base in Binary Verification
… The first contribution targets the validation of OCaml-to-PVS translation -- commonly used to translate instruction-set-architecture (ISA) specifications to PVS -- where the destination language is non-executable. We present a methodology called OPEV to validate the translation between OCaml and …
-
iASTD, un interpréteur d'ASTD
… spécifiée, à leur implémentation dans le langage oCaml, en passant par l'introduction d'algorithmes de Kappa optimisation pour l'exécution des opérateurs quantifiés. Les tests fonctionnels et les tests de performance sont également présentés.
-
SibylFuzzer : stateful fuzzing for file systems
… file system. I implemented SibylFuzzer in OCaml and performed all tests on a Linux file system.
-
Verifying Correctness of the Number Theoretic Transform and Fast Number Theoretic Transform in F⋆
… programming language that extracts to OCaml, and shows that we can use the NTT to perform polynomial multiplications. We provide an implementation of the Cooley-Tukey fast NTT algorithm and a proof that it matches the original NTT specification. This thesis also presents a …
-
Symbolic semantics for CSP
… It also gives us the ability to extract Ocaml code for an HCSP-based simulator directly from Isabelle.
-
Strongly typed, compile-time safe and loosely coupled data persistence
… relational framework, called Qanat, in the OCaml programming language and using a loosely coupled SQL database. We further report experimental results obtained by running a number of benchmark tests, and compare the resulting Qanat applications with the equivalent, raw database driver based …
-
Program Synthesis With Types
… because programs in richly-typed languages like OCaml and Haskell are known for ``writing themselves'' once the programmer gets the types correct. In light of this observation, can we use type theory to build more expressive and efficient type-directed synthesis systems for this domain of …
-
Relational compilation: Functional-to-imperative code generation for performance-critical applications
… them to a similar language (like Coq to OCaml) or by proving them equivalent to deeply embedded implementations (like C programs). Traditionally, the first approach is automated but produces unverified programs with average performance, and the second approach is manual but produces …
-
Low-level cross-language post-link optimisation
… both high-level and low-level languages, such as OCaml, Rust and C. The representation is generated through custom compiler backends and assembled into modules carrying whole program information through a specialised toolchain, before optimisations are applied and executable machine code is …
-
Polarized substructural session types
… relatively full featured interpreter written in OCaml; a fragment of SILL as an embedded domain specific language in Haskell; and a cleaner version of the same in Idris. Lastly, we show that Liquid Types and Session Types are compatible. This gives us one notion of a dependently session typed …
-
Term rewriting with built-in numbers and collection data structures
… programming languages such as Maude or OCaml. This dissertation introduces a new class of term rewrite systems that addresses both of these drawbacks and thus makes it possible to accurately model computer programs using a high level of abstraction in a natural formalism. Then, the …