Type checking in the presence of meta-variables (2008)
Abstract. In this paper we present a type checking algorithm for a dependently typed logical framework extended with meta-variables. It is common for such frameworks to accept that unification...
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...
Abstract. Functional generic programming is an area of research concerning programs parameterized by types. Such parameterization is a powerful method of abstraction that allows the programmer to...
Towards a practical programming language based on dependent type theory (2007)
Ulf Norell, Ulf Norell, C Ulf Norell
Thesis for the degree of Doctor of Philosophy
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...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a first-order theorem prover. Its main purpose is to keep track...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a firstorder theorem prover. Its main purpose is to keep track of...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a firstorder theorem prover. Its main purpose is to keep track of...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a firstorder theorem prover. Its main purpose is to keep track of...
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...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a first-order theorem prover. Its main purpose is to keep track...
Implementing Functional Generic Programming Ulf Norell (2004)
Abstract Functional generic programming extends functional programming with the ability to parameterize functions on the structure of a datatype. This allows a programmer to implement certain...
Polytypic programming in Haskell (2003)
A polytypic (or generic) program captures a common pattern of computation over dierent datatypes by abstracting over the structure of the datatype. Examples of algorithms that can be dened...
Polytypic programming in Haskell (2003)
A polytypic (or generic) program captures a common pattern of computation over dierent datatypes by abstracting over the structure of the datatype. Examples of algorithms that can be dened...
Functional generic programming and type theory (2002)
2 3 Abstract. Functional generic programming is an area of research concerning programs parameterized by types. Such parameterization is a powerful method of abstraction that allows the programmer to...