Marcin Benke, Rozprawa Doktorska, Uniwersytet Warszawski, Informatyki Mechaniki
1.1 Types and programs....................... 1
development in Martin-Löf Type Theory (extended abstract) (2008)
Strategies for interactive proof and program
and Reasoning about Programs—Mechanical verification (2008)
Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell
Proof assistants based on dependent type theory are closely related to functional programming languages, and so it is tempting to use them to prove the correctness of functional programs. In this...
Fix-point Equations for Well-Founded Recursion in Type Theory (2007)
Peter Aczel, Abstracts Aarne Ranta, Marcin Benke, Antonia Balaa
A more general type theoretic interpretation of constructive set theory
Verifying Haskell programs using constructive type theory (2005)
Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell
Abstract Proof assistants based on dependent type theory are closely relatedto functional programming languages, and so it is tempting to use them to prove the correctness of functional programs. In...
Verifying Haskell programs using constructive type theory (2005)
Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell
Abstract Proof assistants based on dependent type theory are closely relatedto functional programming languages, and so it is tempting to use them to prove the correctness of functional programs. In...
Universes for Generic Programs and Proofs in Dependent Type Theory (2003)
Marcin Benke, Peter Dybjer, Patrik Jansson
We show how to write generic programs and proofs in MartinL of type theory. To this end we consider several extensions of MartinL of's logical framework for dependent types. Each extension has a...
Universes for Generic Programs and Proofs in Dependent Type Theory (2003)
Marcin Benke, Peter Dybjer, Patrik Jansson
We show how to write generic programs and proofs in MartinL of type theory. To this end we consider several extensions of MartinL of's logical framework for dependent types. Each extension has...
Some tools for computer-assisted theorem proving in MartinL of type theory (2001)
Abstract. We propose some tools facilitating interactive proof and program development in the proof editor Alfa based on Martin-Löf Type Theory, in particular a tool for equality reasoning supported...
Some tools for computer-assisted theorem proving in MartinL of type theory (2001)
Abstract. We propose some tools facilitating interactive proof and program development in the proof editor Alfa based on Martin-Löf Type Theory, in particular a tool for equality reasoning supported...