dc.contributor.author Howse, Samuel. en_US dc.date.accessioned 2014-10-21T12:37:39Z dc.date.available 2014-10-21T12:37:39Z dc.date.issued 2007 en_US dc.identifier.other AAINR19613 en_US dc.identifier.uri http://hdl.handle.net/10222/54853 dc.description NummSquared 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.description Set 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.description A soundness theorem for NummSquared is proved. en_US dc.description Usual 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.description For 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.description As 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.description Thesis (Ph.D.)--Dalhousie University (Canada), 2007. en_US dc.language eng en_US dc.publisher Dalhousie University en_US dc.publisher en_US dc.subject Computer Science. en_US dc.title NummSquared 2006a0 Explained, including a new well-founded functional foundation for logic, mathematics and computer science. en_US dc.type text en_US dc.contributor.degree Ph.D. en_US
﻿ Find Full text