|
Click on a project in the table below for all publications registered to that project.
Project AFM4: Advancing the Real Use of Proof Assistants
2009
- N. Raja, A Asperti, J.H. Geuvers. Social processes, program verification and all that. athematical Structures in Computer Science, 19, pp 877-896, 2009.
- J.H. Geuvers, L.E. Mamane, J.H. McKinna. A Logically Saturated Extension of lambda-bar-mu-mu-tilde. In Proceedings of the 16th Symposium, 8th International Conference, pp. 405-421, 2009.
- J.H. Geuvers. Introduction to Type Theory. In A. Bove, L. Soares Barbosa, A. Pardo, J. Sousa Pinto (Eds.), Language Engineering and Rigorous Software Development (International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24-March 1, 2008, Revised Tutorial Lectures). (Lecture Notes in Computer Science, Vol. 5520, pp. 1-56). Berlin: Springer, 2009.
- J.H. McKinna, Dhr. E.E. van der Weegen. A Machine-checked Proof of the Average-case Complexity of Quicksort in Coq.. In Types for Proofs and Programs: International Conference, TYPES 2008, pp. 256-271, 2009.
- K. Hammond, E. Brady, S. Bhatti, J.H. McKinna. Domain Specific Languages (DSLs) for Network Protocols. In Proceedings of the 2009 29th IEEE International Conference on Distributed Computing Systems Workshops, pp. 208-213, 2009.
- R. O'Connor, Drs. C.S. Kaliszyk. Computing with Classical Real Numbers. Journal of Formalized Reasoning, Vol 2, No 1, pp. 27-39, 2009.
- H. Geuvers "Proof Assistants: history, ideas and future" , in Sadhana Journal, Academy Proceedings in Engineering Sciences, Special Issue on Interactive Theorem Proving and Proof Checking, Indian Academy of Sciences, Vol 34, part 1, February 2009, pp 3-25.
- H. Geuvers "Introduction to Type Theory", in Proceedings of the International Summer School on Language Engineering and Rigorous Software Development February 25 - March 1, 2008, Piriapolis, Uruguay, organised by the EU LerNet ALFA project, LNCS Springer 2009.
- Eelis van der Weegen and James McKinna, "A Machine-checked Proof of the Average-case Complexity of Quicksort in Coq", In Stefano Berardi, Ferruccio Damiani and Ugo De'Liguoro (eds.), Proceedings of TYPES 2008, LNCS 5497, Springer 2009.
2008
- Pierre Corbineau "A declarative language for the Coq proof assistants." In: Types 2007: Types for Proofs and Programs. 2008.
- Adam Koprowski and Johannes Waldmann "Arctic Termination ... Below Zero", In Proceedings of the 19th International Conference on Rewriting Techniques and Applications, (RTA '08), Hagenberg, Austria, LNCS 5117, Springer.
- Adam Koprowski and Hans Zantema "Certification of Proving Termination of Term Rewriting by Matrix Interpretations", In Proceedings of the 34th International Conference on Current Trends in Theory and Practice of Computer Science, (SOFSEM '08), Nový Smokovec, Slovakia, Geffert, V.; Karhumäki, J.; Bertoni, A.; Preneel, B.; Návrat, P.; Bieliková, M. (Eds.), LNCS 4910 Springer.
- Milad Niqui, Olga Tveretina, "Modular Development of Hybrid Systems for Verification in Coq", In M. Egerstedt and B. Mishra (Eds.), Proceedings of the 11th International Conference on Hybrid Systems: Computation and Control (HSCC'08) LNCS 4981, Springer.
- S. Barry Cooper and Herman Geuvers and Anand Pillay and Jouko A. Väänänen "Preface." In: Ann. Pure Appl. Logic. 156 (1). 2008. pp. 1-2.
- H. Geuvers and F. Wiedijk. A logical framework with explicit conversions. In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, Cork, Ireland. Edited by Carsten Schürmann. 2008. pp. 33-47.
- H. Geuvers and I. Loeb. Deduction Graphs with Universal Quantification. In: Proceedings of TERMGRAPH 2007. Edited by I. Mackie and D. Plump. 2008. pp. 93-108.
2007
- H. Geuvers, I. Loeb Natural Deduction via Graphs: Formal Definition and Computation Rules Mathematical Structures in Computer Science (Special Issue on Theory and Applications of Term Graph Rewriting), Volume 17, Issue 03, pp 485-526, 2007.
- Pierre Corbineau. A Declarative Language for the Coq Proof Assistant. (Department of Computer Science, University of Kaiserslautern technical report Technical Report 364/07), August 2007
- O.Heling-Tveretina and G. Provan. On Approximate Knowledge Compilation with Weighted Decision Diagrams. In: Proceedings of International Conference on Artificial Intelligence, USA, June 25-28, 2007
- H. Geuvers. Computer-ondersteund redeneren: de boekhouder steunt de denker (Dutch). March 9, 2007
- Bas Spitters, Herman Geuvers, Milad Niqui, and Freek Wiedijk. Preface to the special issue: Constructive analysis, types and exact real numbers. In: Mathematical Structures in Computer Science (volume 17, number 1, pages 1), 2007
- Pierre Corbineau and Cezary Kaliszy. Cooperative Repositories for Formal Proofs - A Wiki-Based Solution. In: Towards Mechanized Mathematical Assistants (volume 4573, pages 221-234), LNCS, Springer, 2007
- Bahareh Badban, Jaco van de Pol, Olga Tveretina, and Hans Zantema. Generalizing DPLL and satisfiability for equalities. In: Information and Computation (volume 205, number 8, pages 1188-1211), 2007
- H. Geuvers. Computer-ondersteund redeneren: de boekhouder steunt de denker (Dutch), inaugural speech. 2007 Note: Radboud University Nijmegen, ISBN 978-90-9021687-4
- Herman Geuvers. (In)consistency of Extensions of Higher Order Logic and Type Theory. In: Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers (Edited by Thorsten Altenkirch and Conor McBride) (volume 4502, pages 140-159), Lecture Notes in Computer Science, Springer, 2007
- Pierre Corbineau. Deciding Equality in the Constructor Theory. In: Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers (Edited by Thorsten Altenkirch and Conor McBride) (volume 4502, pages 78-92), Lecture Notes in Computer Science, Springer, 2007
- Herman Geuvers, Milad Niqui, Bas Spitters, and Freek Wiedijk. Constructive analysis, types and exact real numbers. In: Mathematical Structures in Computer Science (volume 17, number 1, pages 3-36), 2007
2006
- A. Asperti, H. Geuvers, I. Loeb, L. Mamane, and C. Sacerdoti Coen. An Interactive Algebra Course with Formalised Proofs and Definitions. In: Proceedings of the Fourth Conference Mathematical Knowledge Management (Edited by M. Kohlhase) (volume 3863, pages 315-329), Lecture Notes in Artificial Intelligence, Springer, 2006
- Herman Geuvers and Iris Loeb. From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions. In: Mathematical Foundations of Computer Science 2006, 31st International Symposium, MFCS 2006, Stará Lesná, Slovakia, August 28-September 1, 2006, Proceedings (Edited by Rastislav Kralovic and Pawel Urzyczyn) (volume 4162, pages 39-57), Lecture Notes in Computer Science, Springer, 2006
- L. Mamane and H. Geuvers. A Document-Oriented Coq Plugin for TEXmacs. In: Mathematical User-Interfaces Workshop 2006, 2006, St Anne's Manor, Workingham, UK,
|
