swMATH ID: 968
Software Authors: Långbacka, Thomas; Ruks̆ėnas, Rimvydas; von Wright, Joakim
Description: Window inference is a method for contextual rewriting and renement supported by the HOL Window Inference Library. This paper describes a userfriendly interface for window inference. The interface permits the user to select subexpressions by pointing and clicking and to select transformations from menus. The correctness of each transformation step is proved automatically by the HOL system. The interface can be tailored to particular userdened theories. One such extension for program renement is described.
Homepage: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=
Related Software: Isabelle; DiskPaxos; Tree Automata; Archive Formal Proofs; Collections; GUItar; FAdo; Scala; Isabelle/HOL; HOL; ML; Theorema; Isabelle/Isar; MAYA; PVS; TAS; IsaWin; HOL90
Referenced in: 7 Publications

Referencing Publications by Year