Hill, Steve, Thompson, Simon (1995) Miranda in Isabelle. In: Paulson, Lawrence C., ed. Preceedings of the first Isabelle Users Workshop. University Of Cambridge Computer Laboratory Technical Reports Series (397). pp. 122-135. (KAR id:21247)
|
PDF
Language: English |
|
|
Click to download this file (97kB)
Preview
|
Preview |
|
This file may not be suitable for users of assistive technology.
Request an accessible format
|
|
|
Postscript
Language: English |
|
|
Click to download this file (119kB)
Preview
|
Preview |
|
This file may not be suitable for users of assistive technology.
Request an accessible format
|
|
Abstract
This paper describes our experience in formalising arguments about the Miranda functional programming language in Isabelle. After explaining some of the problems of reasoning about Miranda, we explain our two different approaches to encoding Miranda in Isabelle. We conclude by discussing some shorter examples and a case study of reasoning about hardware.
| Item Type: | Conference or workshop item (UNSPECIFIED) |
|---|---|
| Uncontrolled keywords: | Miranda verification Isabelle |
| Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
| Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
| Depositing User: | Mark Wheadon |
| Date Deposited: | 19 Aug 2009 19:49 UTC |
| Last Modified: | 16 Nov 2021 09:59 UTC |
| Resource URI: | https://kar.kent.ac.uk/id/eprint/21247 (The current URI for this page, for reference purposes) |
| Thompson, Simon: |
 https://orcid.org/0000-0002-2350-301X
|
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):
Download Statistics
Download Statistics
