77 citations
Showing 2009 · cs.LOShow all
2 papers · 2 filters
cs.LO2009
A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables
Tristan Crolard, Emmanuel Polonowski
We formally specified the type system and operational semantics of LOOPw with Ott and Isabelle/HOL proof assistant. Moreover, both the type system and the semantics of LOOPw have b…
cs.LO2009
Deriving SN from PSN: a general proof technique
Emmanuel Polonowski
In the framework of explicit substitutions there is two termination properties: preservation of strong normalization (PSN), and strong normalization (SN). Since there are not easil…