Practical and Sound Equality Tests, Automatically Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi

Grégoire, B; Léchenet, JC; Tassi, E

Grégoire, B (通讯作者),Univ Cote Dazur, Inria, Sophia Antipolis, France.

PROCEEDINGS OF THE 12TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2023, 2023; (): 167

Abstract

In this paper we describe the design and implementation of feqb, a tool that synthesizes sound equality tests for inductive data types in the dependen......

Full Text Link