31 citations · 133 across the 23 of their papers we have counts for
4 papers · 1 filter
About the efficient reduction of lambda terms
Andrea Asperti
There is still a lot of confusion about "optimal" sharing in the lambda calculus, and its actual efficiency. In this article, we shall try to clarify some of these issues.
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen +1
The paper describes the refinement algorithm for the Calculus of (Co)Inductive Constructions (CIC) implemented in the interactive theorem prover Matita. The refinement algorithm is…
Superposition as a logical glue
Andrea Asperti, Enrico Tassi
The typical mathematical language systematically exploits notational and logical abuses whose resolution requires not just the knowledge of domain specific notation and conventions…
Smart matching
Andrea Asperti, Enrico Tassi
One of the most annoying aspects in the formalization of mathematics is the need of transforming notions to match a given, existing result. This kind of transformations, often base…