Program Derivation by Proof Transformation, CMU, issue.3, 1993. ,
A Content Based Mathematical Search Engine: Whelp, Lecture Notes in Computer Science, vol.3839, issue.3, pp.17-32, 2006. ,
DOI : 10.1007/11617990_2
User Interaction with the Matita Proof Assistant, Journal of Automated Reasoning, vol.11, issue.3, pp.109-139, 2007. ,
DOI : 10.1007/s10817-007-9070-5
Towards an evolutionary formal softwaredevelopment using CASL, Lecture Notes In Computer Science, issue.3, pp.73-88, 2000. ,
A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993. ,
DOI : 10.1145/138027.138060
Management of change in structured verification, Proceedings ASE 2000. Fifteenth IEEE International Conference on Automated Software Engineering, pp.23-34, 2000. ,
DOI : 10.1109/ASE.2000.873647
MBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems, Journal of Symbolic Computation, vol.32, issue.4, pp.365-402, 2001. ,
DOI : 10.1006/jsco.2000.0468
Proofs and refutations (IV) The British Journal for the Philosophy of Science, pp.296-342, 1964. ,
Towards a mechanized metatheory of standard ml, POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.173-184, 2007. ,
Fine-Granular Version Control & Redundancy Resolution, LWA Conference Proceedings (FGWM), pp.1-8, 2008. ,
Documenting and automating collateral evolutions in linux device drivers, ACM SIGOPS Operating Systems Review, vol.42, issue.4, pp.247-260, 2008. ,
DOI : 10.1145/1357010.1352618
URL : https://hal.archives-ouvertes.fr/inria-00123142
System Description: Twelf ??? A Meta-Logical Framework for Deductive Systems, Lecture Notes in Computer Science, vol.1, issue.3, pp.202-206, 1999. ,
DOI : 10.1007/3-540-48660-7_14