Maps abstract computational structures to real-world FriCAS code This allows FriCAS domains to be created from an instance of Lambda it also allows FriCAS categories to be created from an instance of intuitionisticLogic. So by the Curry-Howard isomorphism we can coerce to the intuitionisticLogic from Lambda. This gives an isomorphism where theorems in intuitionistic logic correspond to type signatures in combinatory logic and programs in intuitionistic logic correspond to the proofs of those theorems in combinatory logic. As an example of this in Haskell see “Djinn, a theorem prover in Haskell, for Haskell” here: http://lambda-the-ultimate.
org/node/1178 see also: Philip Wadler - Theorems for free! http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html