Showing cs.PLShow all
2 papers · 1 filter
cs.PL2025
Compiling Gradual Types with Evidence
José Luis Romero, Cristóbal Isla, Matías Toro +1
Efficiently supporting sound gradual typing in a language with structural types is challenging. To date, the Grift compiler is the only close-to-the-metal implementation of gradual…
cs.PL2023
Securing Verified IO Programs Against Unverified Code in F*
Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu +4
We introduce SCIO*, a formally secure compilation framework for statically verified partial programs performing input-output (IO). The source language is an F* subset in which a ve…