Impredicative Observational Equality

Pujet, L; Tabareau, N

Pujet, L (通讯作者),INRIA, Gallinette Project Team, Nantes, France.

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2023; 7 (POPL):

Abstract

In dependent type theory, impredicativity is a powerful logical principle that allows the definition of propositions that quantify over arbitrarily la......

Full Text Link