An Architecture for Analysis

摘要: We propose an architecture controlled by a thin computational layer designed to tightly correspond with the lambda calculus, drawing on principles of functional programming bring assembly much closer myriad reasoning frameworks and specification languages. This approach allows assembly-level verified versions critical code operate safely in tandem arbitrary without need for large supporting trusted computing bases.