NaR ...
Arthur Scott
Higher-order Logic, e.g. Agda, can protect the programmer from programming errors.
posit ™ and Agda Verified Reversible Programming for Verified Lossless Compression, and Agda no hotspots Bespoke Computationally Intensive Kernel Processors.
“DRAFT: Verified Technology Mapping in an Agda DSL for Circuit Design
Circuit refinement through gate and data concretisation…
λπ-Ware, a typed domain-specific language for the description, specification, simulation and synthesis of digital circuits embedded in the dependently typed programming language Agda. Crucially, we show how to use Agda’s module system to parametrise λπ-Ware developments by the choice of primitive gates used in circuit definitions, as well as a base type for the type universe of circuit I/O. …”
João Paulo Pizani Flor and Wouter Swierstra Universiteit Utrecht Utrecht, The Netherlands
“...Agda supports formal verification of program properties, and the compiler for our reversible language (which is implemented as an Agda macro), produces not just an encoder/decoder pair of functions but also a proof that they are inverse to one another. Thus users of the language get formal verification ‘for free’. …
The potential advantages of using Flipper are significant—the amount of user code is reduced, and accidental violation of the inverse property (a common cause of bugs in lossless compression) is no longer possible. …" James Townsend and Jan-Willem van de Meent University of Amsterdam
Arthur Scott
[PDF] Verified Compilation and Optimization of Floating-Point Kernels
to produce machine code that preserves the behavior of the source code. Trusting a
verified compiler is easy. A rigorous machine-checked proof shows that the compiler …