search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
57 stars 19 forks source link

translate binders to Isabelle #428

Open sternk opened 10 years ago

sternk commented 10 years ago

Reported by lschrode and assigned to maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/428

The notation for monads and the monad-based Hoare logic needs to be implemented. The syntax is described in the HasCASL overview. We need both the syntax and some translations, one into HasCASL that just translates out the abbreviations as described in the paper, and one into Isabelle/HOL that keeps the syntax, and of course then has the definitions in the Isabelle theory.

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/428#comment:1

The do-notation can be solved using binders (#447), but this binders still need to be translated to Isabelle. Maybe all terms of the form p >>= \ x . q can be translated using the corresponding binder, otherwise two intermediate representations of terms must be kept.