Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Matthews, Seán

dblp



Editor(s):

Paulson, Lawrence C.

dblp



BibTeX cite key*:

Matthews96b

Title, Booktitle

Title*:

Implementing $\textrm FS_0$ in Isabelle: Adding Structure at the Metalevel

Booktitle*:

Design and Implementation of Symbolic Computation Systems (DISCO'96)

Event, URLs

URL of the conference:


URL for downloading the paper:


Event Address*:

Karlsruhe, Germany

Language:

English

Event Date*
(no longer used):

September 18-20

Organization:

DISCO

Event Start Date:

17 July 2019

Event End Date:

17 July 2019

Publisher

Name*:

Springer

URL:


Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

1128

Number:


Month:

September

Pages:

228-239

Year*:

1996

VG Wort Pages:


ISBN/ISSN:

3540616977

Sequence Number:


DOI:




Note, Abstract, ©


(LaTeX) Abstract:

Often the theoretical virtue of simplicity in a theory does not
fit with the practical necessities of use. An example of this
is Feferman's FS0, a theory of inductive definitions which is
very simple, but seems to lack all practical facilities.
We present an implementation in the Isabelle generic theorem
prover. We show that we can use the facilities available there
to provide all the complex structuring facilities we need
without compromising the simplicity of the original theory.
The result is a thoroughly practical implementation. We
further argue that it is unlikely that a custom implementation
would be as effective.



Download
Access Level:


Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Audience:

experts only

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat



BibTeX Entry:

@INPROCEEDINGS{Matthews96b,
AUTHOR = {Matthews, Se{\'a}n},
EDITOR = {Paulson, Lawrence C.},
TITLE = {Implementing {$\textrm {FS}_0$} in {Isabelle}: Adding Structure at the Metalevel},
BOOKTITLE = {Design and Implementation of Symbolic Computation Systems (DISCO'96)},
PUBLISHER = {Springer},
YEAR = {1996},
ORGANIZATION = {DISCO},
VOLUME = {1128},
PAGES = {228--239},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Karlsruhe, Germany},
MONTH = {September},
ISBN = {3540616977},
}


Entry last modified by Uwe Brahm, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Uwe Brahm
Created
03/06/1996 08:55:01 PM
Revisions
9.
8.
7.
6.
5.
Editor(s)
Uwe Brahm
Seán Matthews
Uwe Brahm
Uwe Brahm
Uwe Brahm
Edit Dates
09.05.97 14:23:11
22/04/97 15:09:38
27.03.97 19:44:02
26.03.97 14:23:19
24.03.97 22:39:35