|
Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem ProverFerruccio Guidi
A Proof-Theoretic Account of Primitive Recursion and Primitive IterationLuca Chiarabini,Olivier Danvy
Automated Reasoning in Higher-Order Logic using the TPTP THF InfrastructureGeoff Sutcliffe,Christoph Benzmueller
Genetic Algorithms in Coq: Generalization and Formalization of the crossover operatorConcepción Vidal,Felicidad Aguado,José Luis Doncel,Jose María Molinelli
|
|
