Logic and Dependent Types in the Aldor Computer Algebra System

Thompson, Simon (2001) Logic and Dependent Types in the Aldor Computer Algebra System. In: Symbolic Computation and Automated Reasoning, Aug 06-07, 2000, St Andrews, Scotland. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)

Abstract

We show how the Aldor type system can represent propositions of first-order logic, by means of the 'propositions as types' correspondence. The representation relies on type casts (using pretend) but can be viewed as a prototype implementation of a modified type system with type evaluation reported elsewhere [9]. The logic is used to provide an, axiomatisation of a number of familiar Aldor categories as well as a type of vectors

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: logic dependent type computer algebra Aldor Axiom
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 17:59
Last Modified: 08 Jul 2009 16:24
Resource URI: http://kar.kent.ac.uk/id/eprint/13642 (The current URI for this page, for reference purposes)
  • Depositors only (login required):