Daniel Fridlender, Tuesda Ys, In B, Sp Ring, ...
rtin-L" of typ etheo ry
TYPE THEORY AND FUNCTIONAL PROGRAMMING A WORK PROPOSAL Gustavo Betarte (2007)
Gustun Cs, Gustavo Betarte, Ana Bove, Cristina Cornes, Sylvia Da Rosa, Daniel Fridlender
We propose a series of work areas related to type theory and functional programming. By type theory we mean the formulation of Martin-Lof's set theory using the theory of types as logical...
Daniel Fridlender, Daniel Fridlender, Mia Indrika, Mia Indrika
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...
Do we Need Dependent Types (2000)
Daniel Fridlender, Daniel Fridlender, Daniel Fridlender, Mia Indrika, Mia Indrika, Mia Indrika
Copyright c
Do we Need Dependent Types (2000)
Daniel Fridlender, Mia Indrika
Inspired by [2], we describe a technique for defining, within the Hindley-Milner type system, some functions which seem to require a language with dependent types. We illustrate this by giving a...
An n-ary zipWith in Haskell (1999)
Daniel Fridlender, Mia Indrika
The aim of this note is to present an alternative definition of the zipWith family in the Haskell Library Report [5]. Because of the difficulties in defining a well-typed function with a variable...
An Interpretation of the Fan Theorem in Type Theory (1998)
is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS Report Series publications. Copies may be...
An Interpretation of the Fan Theorem in Type Theory (1998)
Daniel Fridlender, Daniel Fridlender
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...
Higman's Lemma in Type Theory / (1997)
Thesis (doctoral)--University of Göteborg, 1997.
A lambda calculus model of Martin-Löf's theory of types with explicit substitution (1997)
This paper presents a proof-irrelevant model of Martin-Lof's theory of types with explicit substitution; that is, a model in the style of [Smi88], in which types are interpreted as truth values...
Higman's Lemma in Type Theory (1997)
Daniel Fridlender, Daniel Fridlender, Daniel Fridlender
This thesis is about exploring the possibilities of a limited version of Martin-Lof's type theory. This exploration consists both of metatheoretical considerations and of the actual use of that...
Higman's Lemma in Type Theory (1997)
. This paper starts with a brief exploration of the history of Higman's lemma with emphasis on Veldman's recent intuitionistic proof, which established the lemma in its most general form....
Type Theory and Functional Programming: a work proposal (1997)
Gustavo Betarte, Ana Bove, Juan José Cabezas, Guillermo Calderón, Cristina Cornes, Sylvia Da Rosa, ...
We propose a series of work areas related to program verification, type theory and functional programming. The areas presented are: the implementation of an environment for carrying out constructions...
A proof of Higman's lemma by structural induction (1993)
Thierry Coquand, Daniel Fridlender
This paper gives an example of such an inductive proof for a combinatorial problem. While there exist other constructive proofs of Higman's lemma (see for instance [10, 14]), the present...
Ramsey's Theorem in Type Theory (1993)
We present formalizations of constructive proofs of the Intuitionistic Ramsey Theorem and Higman's Lemma in Martin-Lof's Type Theory. We analyze the computational content of these proofs...
BRICS Basic Research in Computer Science An n-aryzipWith in Haskell
Daniel Fridlender, Mia Indrika, Daniel Fridlender, Mia Indrika
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...
This document in subdirectoryRS/01/10/ Do we need dependent types? ∗
Daniel Fridlender, Mia Indrika, Copyright C, Daniel Fridlender, Mia Indrika, Daniel Fridlender, ...
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...