6 papers
Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version
Harold Carr, Christopher Jenkins, Mark Moir +2
LibraBFT is a Byzantine Fault Tolerant (BFT) consensus protocol based on HotStuff. We present an abstract model of the protocol underlying HotStuff / LibraBFT, and formal, machine-…
Relational Type Theory (All Proofs)
Aaron Stump, Benjamin Delaware, Christopher Jenkins
This paper introduces Relational Type Theory (RelTT), a new approach to type theory with extensionality principles, based on a relational semantics for types. The type constructs o…
Efficient lambda encodings for Mendler-style coinductive types in Cedille
Christopher Jenkins, Aaron Stump, Larry Diehl
In the calculus of dependent lambda eliminations (CDLE), it is possible to define inductive datatypes via lambda encodings that feature constant-time destructors and a course-of-va…
Elaborating Inductive Definitions and Course-of-Values Induction in Cedille
Christopher Jenkins, Colin McDonald, Aaron Stump
In the Calculus of Dependent Lambda Eliminations (CDLE), a pure Curry-style type theory, it is possible to generically λ-encode inductive datatypes which support course-of-values (…
Course-of-Value Induction in Cedille
Denis Firsov, Larry Diehl, Christopher Jenkins +1
In the categorical setting, histomorphisms model a course-of-value recursion scheme that allows functions to be defined using arbitrary previously computed values. In this paper, w…
Spine-local Type Inference
Christopher Jenkins, Aaron Stump
We present spine-local type inference, a partial type inference system for inferring omitted type annotations for System F terms based on local type inference. Local type inference…