Position paper: A real Semantic Web for mathematics deserves a real semantics (2009)
P. Corbineau, H. Geuvers, C. Kaliszyk, J. Mckinna, F. Wiedijk
Abstract. Mathematical documents, and their instrumentation by computers, have rich structure at the layers of presentation, metadata and semantics, as objects in a system for formal mathematical...
Position paper: A real Semantic Web for mathematics deserves a real semantics (2009)
P. Corbineau, H. Geuvers, C. Kaliszyk, J. Mckinna, F. Wiedijk
Abstract. Mathematical documents, and their instrumentation by computers, have rich structure at the layers of presentation, metadata and semantics, as objects in a system for formal mathematical...
Proof Assistants: history, ideas and future (2009)
In this paper we will discuss the fundamental ideas behind proof assistants: What are they and what is a proof anyway? We give a short history of the main ideas, emphasizing the way they ensure the...
AFM4 Collected Scientific Publications: 2006 – 2007 References (2008)
A. Asperti, H. Geuvers, I. Loeb, L. Mamane, C. Sacerdoti, Coen An, ...
[2] Pierre Corbineau. Deciding equality in the constructor theory. In Types for Proofs and Programs
INFORMATION SOCIETY TECHNOLOGIES (2008)
Ist Programme, A. Asperti, Y. Bertot, H. Geuvers, E. Gimenez, H. Herbelin, ...
Equational Reasoning via Partial Re ection (2007)
H. Geuvers, F. Wiedijk, J. Zwanenburg
Abstract. We modify the re ection method to enable it to deal with partial functions like division. The idea behind re ection is to program a tactic for a theorem prover not in the implementation...
Equational Reasoning via Partial Reflection (2000)
H. Geuvers, F. Wiedijk, J. Zwanenburg
. We modify the reection method to enable it to deal with partial functions like division. The idea behind reection is to program a tactic for a theorem prover not in the implementation language but...
Equational reasoning via partial reflection (2000)
H. Geuvers, F. Wiedijk, J. Zwanenburg
Abstract. We modify the reflection method to enable it to deal with partial functions like division. The idea behind reflection is to program a tactic for a theorem prover not in the implementation...
A Simple Model Construction for the Calculus of Constructions (1996)
. We present a model construction for the Calculus of Constructions (CC) where all dependencies are carried out in a set-theoretical setting. The Soundness Theorem is proved and as a consequence of...