Benutzer: Gast  Login
Titel:

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

Dokumenttyp:
Technical Report
Autor(en):
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...     »
Stichworte:
Interactive proof; theory interpretation; Isabelle
Jahr:
2006
Jahr / Monat:
2006-04-01 00:00:00
Seiten/Umfang:
17
 BibTeX