Now showing items 1-1 of 1

• #### Extracting Efficient Code From Constructive Proofs ﻿

(Cornell University, 1986-06)
Extraction is a technique for producing verified programs. A proof of $\forall chi : T \ldot \exists y : T' \ldot F$ corresponds to a function $f$ of type $T \rightarrow T'$ that maps every $\chi$ of type $T$ to a $y$ ...