User: Guest  Login
Title:

Interpretation of Locales in Isabelle:\\Managing Dependencies between Locales

Document type:
Technical Report
Author(s):
Clemens Ballarin
Abstract:
Locales are the theory development modules of the Isabelle proof \\ assistant. Interpretation is a powerful technique of theorem reuse \\ which facilitates their automatic transport to other contexts. This \\ paper is concerned with the interpretation of locales in the context of \\ other locales. Our main concern is to make interpretation an effective \\ tool in an interactive proof environment. Interpretation dependencies \\ between locales are maintained explicitly, by means of a development...     »
Keywords:
Interactive proof; theory interpretation; Isabelle
Year:
2006
Year / month:
2006-04-01 00:00:00
Pages:
17
 BibTeX