Show simple item record

dc.contributor.authorHowse, Samuel.en_US
dc.date.accessioned2014-10-21T12:37:39Z
dc.date.available2014-10-21T12:37:39Z
dc.date.issued2007en_US
dc.identifier.otherAAINR19613en_US
dc.identifier.urihttp://hdl.handle.net/10222/54853
dc.descriptionNummSquared Explained is the thesis version of the comprehensive formal document NummSquared 2006a0 Done Formally, which is available at http://nummist.com/poohbist/.en_US
dc.descriptionSet theory is the standard foundation for mathematics, but often does not include rules of reduction for function calls. Therefore, for computer science, the untyped lambda calculus or type theory is usually preferred. The untyped lambda calculus (and several improvements on it) make functions fundamental, but suffer from nonterminating reductions and have partially non-classical logics. Type theory is a good foundation for logic, mathematics and computer science, except that, by making both types and functions fundamental, it is more complex than either set theory or the untyped lambda calculus. This document proposes a new foundational formal language called NummSquared that makes only functions fundamental, while simultaneously ensuring that reduction terminates, having a classical logic, and attempting to follow set theory as much as possible. NummSquared builds on earlier works by John von Neumann in 1925 and Roger Bishop Jones in 1998 that have perhaps not received sufficient attention in computer science.en_US
dc.descriptionA soundness theorem for NummSquared is proved.en_US
dc.descriptionUsual set theory, the work of Jones, and NummSquared are all well-founded. NummSquared improves upon the works of von Neumann and Jones by having reduction and proof, by supporting computation and reflection, and by having an interpreter called NsGo (work in progress) so the language can be practically used. NummSquared is variable-free.en_US
dc.descriptionFor enhanced reliability, NsGo is an F#/C#. NET assembly that is mostly automatically extracted from a program of the Coq proof assistant.en_US
dc.descriptionAs a possible step toward making formal methods appealing to a wider audience, NummSquared minimizes constraints on the logician, mathematician or programmer. Because of coercion, there are no types, and functions are defined and called without proof, yet reduction terminates. NummSquared supports proofs as desired, but not required.en_US
dc.descriptionThesis (Ph.D.)--Dalhousie University (Canada), 2007.en_US
dc.languageengen_US
dc.publisherDalhousie Universityen_US
dc.publisheren_US
dc.subjectComputer Science.en_US
dc.titleNummSquared 2006a0 Explained, including a new well-founded functional foundation for logic, mathematics and computer science.en_US
dc.typetexten_US
dc.contributor.degreePh.D.en_US
 Find Full text

Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record