94
Voted
ICFP
2002
ACM
16 years 12 days ago
2002
ACM
Motivated by applications to proof assistants based on dependent types, we develop and prove correct a strong reducer and equivalence checker for the -calculus with products, sums...