.
Will confirm.
James.
--
Dr. Thorsten Altenkirchphone : (+44) (0)115 84 66516
Lecturer http://www.cs.nott.ac.uk/~txa/
School of Computer Science ITUniversity of Nottingham
This message has been scanned but we cannot guarantee that it and any
attachments are free
Adam Megacz wrote:
Thorsten Altenkirch [EMAIL PROTECTED] writes:
What is Gilmore's ITT (is this Stephen Gilmore, is he doing Types
these days)?
http://www.cs.ubc.ca/spider/gilmore/
http://www.megacz.com/research/papers/logicism.renewed.notes.pdf
To address the problems, we have in the past
Conor McBride wrote:
Hi Sebastian
Sebastian Hanowski wrote:
( f : Fin (suc m) - Fin (suc n) !
let !---!
! restrict _m _n f : Fin m - Fin n )
Should you be able to write a function with this type? I can certainly
write a function from Fin 2 to
elimnators using
well known techniques.
Cheers,
Thorsten
--
Dr. Thorsten Altenkirchphone : (+44) (0)115 84 66516
Lecturer http://www.cs.nott.ac.uk/~txa/
School of Computer Science ITUniversity of Nottingham
This message has been checked for viruses
Yong Luo wrote:
Hi, Conor,
Since you use elimination rule on both arguments, I was expecting four cases
like Thorsten did in the previous email. If you can define the Ackermann
function, then you must be able to define the Majority function. Is there
anything more than the standard
Since you use elimination rule on both arguments, I was expecting
four cases
like Thorsten did in the previous email. Can we define the Ackermann
function like the following form?
Conor used the official version of the Ackermann function, which just
has three lines, while I used my own
Hi Robin,
thank you for your comments. Indeed we are currently revising this
paper, hence your comments are especially welcome.
I've been reading Towards Observational Type Theory. I'm new to type
theory, so I have not been able to understand big chunks of the paper;
hopefully as I read
Hi Conor,
I'm not sure I understand what's going on here.
This happens if you don't type check your definitions. I got carried
away with my non-dependent simplification of the story.
Thank you for actually reading it.
Indeed, in the setoid model we can construct a function
f : A -
Hi Bas,
thank you - indeed this is a very interesting observation. This was
the proof I had in mind when I first claimed that the axiom of choice
is provable in OTT. However, I was deluded in believing that OTT/
predicative topoi exactly characterize the theory of the setoid
model. As you
(http://sneezy.cs.nott.ac.uk/darcs/DTP08/journal.html)
Editors:
Thorsten Altenkirch (Nottingham)
Tarmo Uustalu (Tallinn)
Dependently typed programming is using the power of dependent types to
capture relationships between data
Hi,
we have two fully funded PhD positions in our project on induction-
recursion: one at Swansea (with Anton Setzer) and one at Nottingham
(with me). This would be perfect for people who are interested in the
foundations of Type Theory. See
http://www.cs.nott.ac.uk/~txa/phd.html
Please
11 matches
Mail list logo
