AT
Amin Timany
4 records found
1
Authored
Consider two widely used definitions of equality. That of Leibniz: One value equals another if any predicate that holds of the first holds of the second. And that of Martin-Löf: The type identifying one value with another is occupied if the two values are identical. The former da
...
Scala step-by-step
Soundness for DOT with step-indexed logical relations in Iris
The metatheory of Scala's core type system - the Dependent Object Types (DOT) calculus - is hard to extend, like the metatheory of other type systems combining subtyping and dependent types. Soundness of important Scala features therefore remains an open problem in theory and ...
MoSeL
A general, extensible modal framework for interactive proofs in separation logic
A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant. One of the most advanced such tools is the Iris Proof Mode (IPM) for Coq, which offers a rich set of tactics for making separation-logic proofs look a
...
When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they are cluttered with bookkeepi
...