Inheritance in Higher Order Logic: Modeling and Reasoning

Marieke Huisman; Bart Jacobs

doi:10.1007/3-540-44659-1_19

Inheritance in Higher Order Logic: Modeling and Reasoning

Marieke Huisman, Bart Jacobs

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

12 Citations (Scopus)

Abstract

This paper describes a way of modeling inheritance (in object-oriented programming languages) in higher order logic. This particular approach is used in the LOOP project for reasoning about JAVA classes, with the proof tools PVS and ISABELLE. It relies on nested interface types to capture the superclasses, fields, methods, and constructors of classes, together with suitable casting functions incorporating the difference between hiding of fields and overriding of methods. This leads to the proper handling of late binding, as illustrated in several verification examples.

Original language	English
Title of host publication	Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings
Editors	Mark Aagaard, John Harrison
Publisher	Springer
Pages	301-319
Number of pages	19
ISBN (Electronic)	978-3-540-44659-0
ISBN (Print)	978-3-540-67863-2
DOIs	https://doi.org/10.1007/3-540-44659-1_19
Publication status	Published - 2000
Externally published	Yes
Event	13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000 - Portland, United States Duration: 14 Aug 2000 → 18 Aug 2000 Conference number: 13

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	1869

Conference

Conference	13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000
Abbreviated title	TPHOLs 2000
Country/Territory	United States
City	Portland
Period	14/08/00 → 18/08/00

Access to Document

10.1007/3-540-44659-1_19

Cite this

Huisman, M., & Jacobs, B. (2000). Inheritance in Higher Order Logic: Modeling and Reasoning. In M. Aagaard, & J. Harrison (Eds.), Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings (pp. 301-319). (Lecture Notes in Computer Science; Vol. 1869). Springer. https://doi.org/10.1007/3-540-44659-1_19

@inproceedings{f37abe863a4446f7a7273f8d5dbcdac8,

title = "Inheritance in Higher Order Logic: Modeling and Reasoning",

abstract = "This paper describes a way of modeling inheritance (in object-oriented programming languages) in higher order logic. This particular approach is used in the LOOP project for reasoning about JAVA classes, with the proof tools PVS and ISABELLE. It relies on nested interface types to capture the superclasses, fields, methods, and constructors of classes, together with suitable casting functions incorporating the difference between hiding of fields and overriding of methods. This leads to the proper handling of late binding, as illustrated in several verification examples.",

author = "Marieke Huisman and Bart Jacobs",

year = "2000",

doi = "10.1007/3-540-44659-1_19",

language = "English",

isbn = "978-3-540-67863-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "301--319",

editor = "Mark Aagaard and John Harrison",

booktitle = "Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings",

address = "Germany",

note = "13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000, TPHOLs 2000 ; Conference date: 14-08-2000 Through 18-08-2000",

}

Huisman, M & Jacobs, B 2000, Inheritance in Higher Order Logic: Modeling and Reasoning. in M Aagaard & J Harrison (eds), Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1869, Springer, pp. 301-319, 13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000, Portland, Oregon, United States, 14/08/00. https://doi.org/10.1007/3-540-44659-1_19

Inheritance in Higher Order Logic: Modeling and Reasoning. / Huisman, Marieke; Jacobs, Bart.
Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings. ed. / Mark Aagaard; John Harrison. Springer, 2000. p. 301-319 (Lecture Notes in Computer Science; Vol. 1869).

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

TY - GEN

T1 - Inheritance in Higher Order Logic: Modeling and Reasoning

AU - Huisman, Marieke

AU - Jacobs, Bart

N1 - Conference code: 13

PY - 2000

Y1 - 2000

N2 - This paper describes a way of modeling inheritance (in object-oriented programming languages) in higher order logic. This particular approach is used in the LOOP project for reasoning about JAVA classes, with the proof tools PVS and ISABELLE. It relies on nested interface types to capture the superclasses, fields, methods, and constructors of classes, together with suitable casting functions incorporating the difference between hiding of fields and overriding of methods. This leads to the proper handling of late binding, as illustrated in several verification examples.

AB - This paper describes a way of modeling inheritance (in object-oriented programming languages) in higher order logic. This particular approach is used in the LOOP project for reasoning about JAVA classes, with the proof tools PVS and ISABELLE. It relies on nested interface types to capture the superclasses, fields, methods, and constructors of classes, together with suitable casting functions incorporating the difference between hiding of fields and overriding of methods. This leads to the proper handling of late binding, as illustrated in several verification examples.

U2 - 10.1007/3-540-44659-1_19

DO - 10.1007/3-540-44659-1_19

M3 - Conference contribution

SN - 978-3-540-67863-2

T3 - Lecture Notes in Computer Science

SP - 301

EP - 319

BT - Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings

A2 - Aagaard, Mark

A2 - Harrison, John

PB - Springer

T2 - 13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000

Y2 - 14 August 2000 through 18 August 2000

ER -

Inheritance in Higher Order Logic: Modeling and Reasoning

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this