compCode

computation.spad line 2790 [edit on github]

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

writeCategory: (List ILogic, String, String, String) -> Void

writes a category to a file.

writePackage: (List Lambda Typed, String, String, String, String) -> Void

writes a package to a file.