Verified lexical analysis

Tobias Nipkow

doi:10.1007/bfb0055126

Verified lexical analysis

Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

24 Scopus citations

Abstract

This paper presents the development and verification of a (very simple) lexical analyzer generator that takes a regular expression and yields a functional lexical analyzer. The emphasis is on simplicity and executability. The work was carried out with the help of the theorem prover Isabelle/HOL.

Original language	English
Title of host publication	Theorem Proving in Higher Order Logics - 11th International Conference, TPHOLs 1998, Proceedings
Editors	Jim Grundy, Malcolm Newey
Publisher	Springer Verlag
Pages	1-15
Number of pages	15
ISBN (Print)	3540649875, 9783540649878
DOIs	https://doi.org/10.1007/bfb0055126
State	Published - 1998
Event	11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1998 - Canberra, Australia Duration: 27 Sep 1998 → 1 Oct 1998

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1479
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1998
Country/Territory	Australia
City	Canberra
Period	27/09/98 → 1/10/98

Access to Document

10.1007/bfb0055126

Cite this

Nipkow, T. (1998). Verified lexical analysis. In J. Grundy, & M. Newey (Eds.), Theorem Proving in Higher Order Logics - 11th International Conference, TPHOLs 1998, Proceedings (pp. 1-15). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1479). Springer Verlag. https://doi.org/10.1007/bfb0055126

@inproceedings{d7dbb9da8bbf4310b9e329eb83302a59,

title = "Verified lexical analysis",

abstract = "This paper presents the development and verification of a (very simple) lexical analyzer generator that takes a regular expression and yields a functional lexical analyzer. The emphasis is on simplicity and executability. The work was carried out with the help of the theorem prover Isabelle/HOL.",

author = "Tobias Nipkow",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1998.; 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1998 ; Conference date: 27-09-1998 Through 01-10-1998",

year = "1998",

doi = "10.1007/bfb0055126",

language = "English",

isbn = "3540649875",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "1--15",

editor = "Jim Grundy and Malcolm Newey",

booktitle = "Theorem Proving in Higher Order Logics - 11th International Conference, TPHOLs 1998, Proceedings",

}

Nipkow, T 1998, Verified lexical analysis. in J Grundy & M Newey (eds), Theorem Proving in Higher Order Logics - 11th International Conference, TPHOLs 1998, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1479, Springer Verlag, pp. 1-15, 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1998, Canberra, Australia, 27/09/98. https://doi.org/10.1007/bfb0055126

Verified lexical analysis. / Nipkow, Tobias.
Theorem Proving in Higher Order Logics - 11th International Conference, TPHOLs 1998, Proceedings. ed. / Jim Grundy; Malcolm Newey. Springer Verlag, 1998. p. 1-15 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1479).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Verified lexical analysis

AU - Nipkow, Tobias

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1998.

PY - 1998

Y1 - 1998

N2 - This paper presents the development and verification of a (very simple) lexical analyzer generator that takes a regular expression and yields a functional lexical analyzer. The emphasis is on simplicity and executability. The work was carried out with the help of the theorem prover Isabelle/HOL.

AB - This paper presents the development and verification of a (very simple) lexical analyzer generator that takes a regular expression and yields a functional lexical analyzer. The emphasis is on simplicity and executability. The work was carried out with the help of the theorem prover Isabelle/HOL.

UR - http://www.scopus.com/inward/record.url?scp=84947766526&partnerID=8YFLogxK

U2 - 10.1007/bfb0055126

DO - 10.1007/bfb0055126

M3 - Conference contribution

AN - SCOPUS:84947766526

SN - 3540649875

SN - 9783540649878

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 1

EP - 15

BT - Theorem Proving in Higher Order Logics - 11th International Conference, TPHOLs 1998, Proceedings

A2 - Grundy, Jim

A2 - Newey, Malcolm

PB - Springer Verlag

T2 - 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1998

Y2 - 27 September 1998 through 1 October 1998

ER -

Verified lexical analysis

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this