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 currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. (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: https://kar.kent.ac.uk/id/eprint/13642 (The current URI for this page, for reference purposes)
  • Depositors only (login required):