Showing 2021Show all
3 papers · 1 filter
cs.LO2021
The Multiverse: Logical Modularity for Proof Assistants
Kenji Maillard, Nicolas Margulies, Matthieu Sozeau +2
Proof assistants play a dual role as programming languages and logical systems. As programming languages, proof assistants offer standard modularity mechanisms such as first-class…
cs.PL2021
Approximate Normalization and Eager Equality Checking for Gradual Inductive Families
Joseph Eremondi, Ronald Garcia, Éric Tanter
Harnessing the power of dependently typed languages can be difficult. Programmers must manually construct proofs to produce well-typed programs, which is not an easy task. In parti…
cs.PL2021
Gradual Program Analysis for Null Pointers
Sam Estep, Jenna Wise, Jonathan Aldrich +3
Static analysis tools typically address the problem of excessive false positives by requiring programmers to explicitly annotate their code. However, when faced with incomplete ann…