An Implementation of Type:Type (2008)
Abstract. We present a denotational semantics of a type system with dependent types, where types are interpreted as finitary projections. We prove then the correctness of a type-checking algorithm...
Verifying haskell pro-grams by combining testing and proving (2008)
Peter Dybjer, Qiao Haiyan, Makoto Takeyama
We propose a method for improving confidence in the correctness of Haskell programs by combining testing and proving. Testing is used for debugging programs and specification before a costly proof...
IOS Press A Logical Framework with Dependently Typed Records ∗ (2008)
Thierry Coquand, Chalmers Tekniska Högskola, Makoto Takeyama, Randy Pollack
Our long term goal is a system to formally represent complex structured mathematical objects, and proofs and computation on such objects; e.g. a foundational computer algebra system. Our approach is...
Agate –an Agda-to-Haskell compiler (2008)
Yoshiki Kinoshita, Hiroyuki Ozaki, Makoto Takeyama, Yoshiki Kinoshita
Abstract. We report some features of Agate, a compiler for the dependently typed functional language of Agda proof-assistant. Agate is developed to be an experimental platform for practice of...
A Logical Framework with Dependently Typed Records (2007)
Thierry Coquand, Randy Pollack, Y Pollack, Makoto Takeyama
this paper we propose an extension of Martin-Lof's logical framework [23, 19] with dependently typed records, and present the semantic fou;7 tion and the typechecking algorithm of ou r system....
Combining Testing and Proving in Dependent Type Theory (2003)
Peter Dybjer, Qiao Haiyan, And Makoto Takeyama, Makoto Takeyama
We extend the proof assistant Agda/Alfa for dependent type theory with a modi ed version of Claessen and Hughes' tool QuickCheck for random testing of functional programs. In this way we combine...
Modules as Dependently Typed Records (2002)
Thierry Coquand, Randy Pollack, Y Pollack, Makoto Takeyama
Syntax For expressions, we have fours categories: expressions, sorts, contexts and definitional context. The abstract syntax is e; a = e e j x j s j [x = e]e j [x : a]e j fx : age j e:x j !\Gamma? j...
An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement (1997)
Yoshiki Kinoshita, Peter W. O'hearn, A. John Power, Makoto Takeyama, Robert D. Tennent
We introduce an axiomatic approach to logical relations and data refinement. We consider a programming language and the monad on the category of small categories generated by it. We identify abstract...
An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement (1997)
Yoshiki Kinoshita, Peter W. O'Hearn, A. John Power, Makoto Takeyama, Robert D. Tennent
We introduce an axiomatic approach to logical relations and data refinement. We consider a programming language and the monad on the category of small categories generated by it. We identify abstract...
Universal Structure and a Categorical Framework for Type Theory (1995)
This thesis investigates the possibility of a computer checked language for categories with extra structure; the language is to describe objects and morphisms of those categories and to reason about...
Universal Structure and a Categorical Framework for Type Theory (1995)
This thesis investigates the possibility of a computer checked language for categories with extra structure; the language is to describe objects and morphisms of those categories and to reason about...