Logic of general recursive functional programs

• Program verification in a logical theory of constructions. In J.-P. Jouannaud, editor, Functional Programming Languages and Computer Architecture, pages 334--349. Springer-Verlag, LNCS 201, September 1985. Appears in revised form as Programming Methodology Group Report 26, June 1986.
• (with Herbert Sander) A functional programming approach to the specification and verification of concurrent systems. Formal Aspects of Computing, 1:303--319, 1989.
• Comparing integrated and external logics of functional programs. Science of Computer Programming, 14:59--79, 1990.
• (with Ana Bove and Andres Sicard-Ramirez) Embedding a logical theory of constructions in Agda. In Proceedings of the 2009 ACM SIGPLAN Workshop on Programming Languages Meet Program Verification (PLPV 2009). Savannah, Georgia, USA, 2009.
• Combining interactive and automatic reasoning in first order theories of functional programs (with Ana Bove and Andres Sicard-Ramirez). In FOSSACS 2012.

• Martin-Löf Type Theory and the Logic of Functional Programs, presented at the Workshop on Types for Verification, Amagasaki, Japan, May 2004.
• Interactive and Automatic Theorem Proving in the First Order Theory of Combinators Lecture given in Gothenburg, 30 November 2011.