FRET Proof Framework

Jan 17, 2022·
Laura Titolo
,
Esther Conrad
,
Dimitra Giannakopoulou
,
Thomas Pressburger
,
Aaron Dutle
· 1 min read

Rigorous PVS formalization of the Fretish structured natural language.

It includes a new denotational semantics and a proof of semantic equivalence between Fretish specifications and their temporal logic counterparts computed by Fret.