James Torre - Formally Specified Digital Logic for Pervasively Reconfigurable Computing - λC 2017

Description:

Pervasively Reconfigurable Computing is a project to design reflectively reconfigurable software across the entire computing stack, from the hardware level up. The Universal Cell is a proposed digital logic circuit element that supports reversible, asynchronous, and homogeneously reconfigurable behavior within a single primitive component. The speaker will present a formal specification of the abstract transition system that the UC embodies, using Lamport's Temporal Logic of Actions (TLA+), and verify a simulation of the hardware by translating TLA+ terms into miniKanren, a Scheme logic programming EDSL.