NDLTD logo NDLTD Union Catalog and Global ETD Search

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 3 of 3 for “"Rocq"”.

  1. Prototyping a Scalable Proof Engine

    Rosario, JonMassachusetts Institute of Technology2025

    … theorem provers such as Coq (now known as Rocq) or Lean is painfully slow. These proof assistants rely on proof engines to construct proofs of correctness for given properties, but to our knowledge, there is no widely available proof engine that offers strong performance guarantees. Even …

    mit Repository record

  2. Dependency Tracking and Dependent Types

    Liu, Yiyun2026

    … dissertation have been fully mechanized in the Rocq theorem prover.

    penn Repository record

  3. Formal ᴘ‑Category Theory and Normalisation for Simple Type Theory

    Berry, DavidUniversity of Cambridge2025

    … have been formalised in the proof assistant Rocq.

    cambridge Repository record