Re: [Epigram] first pass problems

2004-09-02 Thread Thorsten Altenkirch
So true' trick? 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 scanned but we cannot guarantee that it and any

Re: [Epigram] Epigram and Type:Type

2004-10-19 Thread Thorsten Altenkirch
. On the Consistency of a Slight Modification of Quine's New Foundations. Synthese, vol 19, pp 250-263. [4] On the Consistency of a Positive Theory. O. Esser. Mathematical Logic Quarterly 45 (1999), pp. 105-116. -- Dr. Thorsten Altenkirchphone : (+44) (0)115 84 66516 Lecturer

Re: [Epigram] Meeting A) or B)

2004-10-20 Thread Thorsten Altenkirch
. 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

Re: [Epigram] Epigram and Type:Type

2004-10-27 Thread Thorsten Altenkirch
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

Re: [Epigram] Things amongst others

2004-11-18 Thread Thorsten Altenkirch
variable binding to model access models to a state. Indeed Epimacs should be written in Epigram, what else? T. -- Dr. Thorsten Altenkirchphone : (+44) (0)115 84 66516 Lecturer http://www.cs.nott.ac.uk/~txa/ School of Computer Science ITUniversity

Re: [Epigram] files

2005-05-24 Thread Thorsten Altenkirch
Venanzio Capretta wrote: Hi, the most basic question about epigram: How do I reprocess a .epi file that I saved? Thank you, Venanzio You load it into an emacs buffer and type C-c C-c. See , see http://www.dur.ac.uk/CARG/epigram/epigram-system.pdf p.6 Cheers, Thorsten This message has

Re: [Epigram] zero not suc

2005-06-24 Thread Thorsten Altenkirch
at 6.1 of http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf Can you complete that proof? Yes, ( n : Nat ! let !--! ! zeronosuc n : not (zero = suc n) ) zeronosuc n = znosuc n Cheers, Thorsten -- Dr. Thorsten Altenkirch

Re: [Epigram] a naught E, non-structural call

2005-10-10 Thread Thorsten Altenkirch
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

Re: [Epigram] Why does not Epigram accept this?

2005-10-22 Thread Thorsten Altenkirch
Hi Lars, Sorry for the disturbance I cause but I still can not get the pairglob function right it seems. The definition I sent you a few days ago used a case construction which is unneccesary in the presence of the selectors (eliminators) globroot and globchild. So I wrote a new pairglob using

[Epigram] [types06] TYPES 2006 workshop

2005-11-07 Thread Thorsten Altenkirch
be invited lectures. Please direct all emails related to TYPES 2006 to [EMAIL PROTECTED] Cheers, The Organisation Comittee Thorsten Altenkirch, James Chapman, Conor McBride, Peter Morris and Wouter Swiestra . -- Dr. Thorsten Altenkirchphone : (+44) (0)115 84 66516 Lecturer

Re: [Epigram] epigram tells me fibs

2005-11-17 Thread Thorsten Altenkirch
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

Re: [Epigram] epigram tells me fibs

2005-11-20 Thread Thorsten Altenkirch
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

Re: [Epigram] epigram tells me fibs

2005-11-20 Thread Thorsten Altenkirch
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

Re: [Epigram] epigram tells me fibs

2005-11-21 Thread Thorsten Altenkirch
Apologies, this email was intended for Yong personally - not for the list. My mistake. Thorsten Thorsten Altenkirch wrote: 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

Re: [Epigram] Definitional equality in observational type theory

2007-01-25 Thread Thorsten Altenkirch
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

Re: [Epigram] Definitional equality in observational type theory

2007-01-29 Thread Thorsten Altenkirch
Hi Robin, The paper says Observational reasoning can be simulated in Intensional Type Theory by the use of setoids, i.e. types with an explicit equivalence relation. I'm not clear on what the differences are between OTT and simulating observational reasoning with setoids in ITT. Clearly OTT

Re: [Epigram] Definitional equality in observational type theory

2007-02-01 Thread Thorsten Altenkirch
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

Re: [Epigram] Definitional equality in observational type theory

2007-02-01 Thread Thorsten Altenkirch
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 -

Re: [Epigram] Definitional equality in observational type theory

2007-02-01 Thread Thorsten Altenkirch
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

[Epigram] CFP: Dependently Typed Programming (FI Special Issue)

2008-06-30 Thread Thorsten Altenkirch
(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

[Epigram] PhD positions at Nottingham Swansea

2009-03-13 Thread Thorsten Altenkirch
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