Deriving Hypercubes of Type Systems for Safe and Verifiable AI
Details
Join us online for “Deriving Hypercubes of Type Systems,” a presentation by Dr. Mike Stay, exploring how an operational theory—a formal description of the basic operations a computational system can perform and how those operations interact—can be used to generate a hypercube of possible type systems. Each dimension of the hypercube represents a different choice about what may depend on what, producing families of computational guardrails that can make neural networks, probabilistic programs, neurosymbolic systems, and self-modifying AGI safer, more systematic, and more verifiable.
More formally, Barendregt’s Lambda Cube organizes typed lambda calculi by enabling different dependencies between terms and types. We show how to derive an analogous hypercube of type systems from an arbitrary finite presentation of an operational theory and a few design choices.
About Mike Stay
Dr. Mike Stay is Director of Research and Development at F1R3FLY.io. He worked as a cryptanalyst, writing dozens of password crackers for AccessData. He spent eight years at Google on their Applied Security Team, where his group developed the JavaScript security API that was later adopted as part of ECMAScript 5. He went on to be CTO of Pyrofex; there he and others developed the Casanova consensus algorithm and demonstrated a blockchain that ran at 140k TPS. He also developed a new cryptanalytic attack allowing him to recover a few hundred thousand dollars of bitcoin from an encrypted Zip file for a client. His research interests hover around the triple point of math, physics, and computer science.