Generic derivation of induction for impredicative encodings in Cedille

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018 ◽

10.1145/3167087 ◽

2018 ◽

Cited By ~ 5

Author(s):

Denis Firsov ◽

Aaron Stump

Download Full-text