2 papers
cs.LO2025
Dependently Sorted Nominal Signatures
Maribel Fernández, Miguel Pagano, Nora Szasz +1
We investigate an extension of nominal many-sorted signatures in which abstraction has a form of instantiation, called generalised concretion, as elimination operator (similarly to…
cs.LO2025
Derivation and Verification of Array Sorting by Merging, and its Certification in Dafny
Juan Pablo Carbonell, José E. Solsona, Nora Szasz +1
We provide full certifications of two versions of merge sort of arrays in the verification-aware programming language Dafny. We start by considering schemas for applying the divide…