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. (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):
