activity
20162022
most citedCompositional pre-processing for automated reasoning in dependent type theory

4 citations · 7 across the 7 of their papers we have counts for

collaborators
Showing cs.PLShow all

1 paper · 1 filter

cs.PL2016

All the λ-Terms are Meaningful for the Infinitary Relational Model

Pierre Vial

Infinite types and formulas are known to have really curious and unsound behaviors. For instance, they allow to type Ω, the auto- autoapplication and they thus do not ensure any fo…