Research Commons
      • Browse 
        • Communities & Collections
        • Titles
        • Authors
        • By Issue Date
        • Subjects
        • Types
        • Series
      • Help 
        • About
        • Collection Policy
        • OA Mandate Guidelines
        • Guidelines FAQ
        • Contact Us
      • My Account 
        • Sign In
        • Register
      View Item 
      •   Research Commons
      • University of Waikato Research
      • Computing and Mathematical Sciences
      • Computer Science Working Paper Series
      • 1994 Working Papers
      • View Item
      •   Research Commons
      • University of Waikato Research
      • Computing and Mathematical Sciences
      • Computer Science Working Paper Series
      • 1994 Working Papers
      • View Item
      JavaScript is disabled for your browser. Some features of this site may not work without it.

      A calculator for supporting derivation in constructive type-theory: PICTCalc

      Reeves, Steve
      Thumbnail
      Files
      uow-cs-wp-1994-08.pdf
      4.794Mb
      Find in your library  
      Citation
      Export citation
      Reeves, S. (1994). A calculator for supporting derivation in constructive type-theory: PICTCalc. (Working paper 94/08). Hamilton, New Zealand: University of Waikato, Department of Computer Science.
      Permanent Research Commons link: https://hdl.handle.net/10289/1137
      Abstract
      PICTCalc is an interactive program written in LPA Prolog which has encoded within it the rules of Martin-Löf's constructive type theory (CTT), a formal system based on the constructive or intuitionistic mathematics of Brouwer, Heyting and others. It allows us to specify and express any total, computable function, so from a computer science point of view we can write both specifications and programs, along with the derivations which lead from one to the other, in a single language. PICTCalc is a more recent version of MacPICT which is itself a reconstruction of PICT [Ham92] and is intended as a test-bed for providing formal support for work within CTT. Many of the developments and improvements were suggested by students since they used the system to work on substantial courseworks. As we shall see, PICTCalc can be used to assist in the development of derivations in CTT and so it is called a derivation assistant (DA). In this paper I show how PICTCalc can be used for supporting derivations in CTT and consider what current experience suggests for future improvement. The examples in this paper will not require any knowledge of CTT since the meaning will either be clear to anyone with experience of logic and programming notations in general or will be explained as necessary.
      Date
      1994-06
      Type
      Working Paper
      Series
      Computer Science Working Papers
      Report No.
      94/08
      Collections
      • 1994 Working Papers [18]
      Show full item record  

      Usage

      Downloads, last 12 months
      59
       
       

      Usage Statistics

      For this itemFor all of Research Commons

      The University of Waikato - Te Whare Wānanga o WaikatoFeedback and RequestsCopyright and Legal Statement