[Initial tree, bibliography mattam@mattam.org**20050228130231] [Tinkering beginning... Matthieu.Sozeau@lri.fr**20050302194031] [Bib and clean correct rules. Matthieu Sozeau **20050307100916] [LaTeX niceties and better rules :) Matthieu Sozeau **20050307222154] [Log wrote, more things to come today. Matthieu Sozeau **20050309152932] [11 mars work Matthieu Sozeau **20050314120943] [before two judgments Matthieu Sozeau **20050316215243 Logs 'till 16 march ] [17 mars Matthieu Sozeau **20050317171141] [23 mars checkpoint Matthieu Sozeau **20050323144837 Divided the tex files, more modular and reusable typing rules, some logs. ] [Cleanup/tidy Matthieu Sozeau **20050323153143] [24 march's work Matthieu Sozeau **20050324174149] [25,30 march work Matthieu Sozeau **20050330140346] [30 mars's work Matthieu Sozeau **20050331074643] [Change i suffix to a Matthieu Sozeau **20050331093125] [Last march's day... lot of work Matthieu Sozeau **20050331161728] [Début 1er avril Matthieu Sozeau **20050401122511] [Pas de blague! Matthieu Sozeau **20050401142757] [before subtyping judgment change Matthieu Sozeau **20050405142201] [Quelques corrections Matthieu Sozeau **20050405174031] [added tex styles to repo Matthieu.Sozeau@lri.fr**20050603091436] [log, some corrections Matthieu.Sozeau@lri.fr**20050603115809] [Resuming work Matthieu.Sozeau@lri.fr**20050610175002 Added macros, rewrote old text, finished some proofs... ] [Forgot to add grammar file Matthieu.Sozeau@lri.fr**20050614120432] [began the slides mattam@mattam.org**20050615151830] [little fix Matthieu Sozeau **20050419082017] [Missing bibtex files Matthieu Sozeau **20050425083052] [Little fixes, now compiles cleanly mattam@mattam.org**20050615182204] [Little fixes, now slides compiles cleanly mattam@mattam.org**20050615182821] [Slides continued, latex fixes mattam@mattam.org**20050616164102] [little latex fix mattam@mattam.org**20050616164241] [Forgot to add grammar macros mattam@mattam.org**20050620161019] [17 june work Matthieu.Sozeau@lri.fr**20050620164837] [add code example qsort Matthieu Sozeau **20050623104934] [Plan du pré-rapport Matthieu Sozeau **20050625101030] [(almost) Monday's work Matthieu Sozeau **20050628022148] [Tuesday's work (day) Matthieu Sozeau **20050628183231] [Tuesday work (night) Matthieu Sozeau **20050629000346 Refactorized some latex code, almost finished short version (begin and end missing) checked first page for typos etc.. TODO: missing figures, rework lambda-cube, references. ] [Fixed bibliography, added missing refs Matthieu.Sozeau@lri.fr**20050629164720] [Forgot to add barras bib file Matthieu.Sozeau@lri.fr**20050630075124] [ToC Matthieu Sozeau **20050630081127] [Corrected until related work Matthieu Sozeau **20050630101431] [Correction done, needs examples etc Matthieu Sozeau **20050630124113] [Fixed missing refs, typesetting Matthieu.Sozeau@lri.fr**20050630153831] [Corrected version, better grammar def Matthieu Sozeau **20050701024741] [Conclusion et explication Gamma' Matthieu Sozeau **20050701111911] [Correction 3 Matthieu.Sozeau@lri.fr**20050701131025] [Last minute fixes Matthieu.Sozeau@lri.fr**20050701162333] [Fixed slides Matthieu Sozeau **20050703003158] [Corrected slides until 'typing' mattam@mattam.org**20050703112414] [Sunday day work, slides almost finished mattam@mattam.org**20050703145637] [Added some figures, interaction mattam@mattam.org**20050703174615] [Fixes from christine Matthieu Sozeau **20050704095149] [Correction with Christine Matthieu.Sozeau@lri.fr**20050704141127] [Slides, handout Matthieu.Sozeau@lri.fr**20050704150544] [Last minute fixes Matthieu Sozeau **20050704210708] [Presentation fixes Matthieu Sozeau **20050705060628] [Cleanup before writing final report Matthieu Sozeau **20050726134001] [Integration of short report into final + proofs, split files Matthieu Sozeau **20050728113145] [Work on proofs Matthieu Sozeau **20050823223805] [Still working on proofs Matthieu Sozeau **20050824115141] [Soundness et completness Matthieu Sozeau **20050825131603] [Split main file parts Matthieu Sozeau **20050825154947] [Begin last proof Matthieu Sozeau **20050830063935] [Corrections... Matthieu Sozeau **20050830104253] [Minor fixes Matthieu.Sozeau@lri.fr**20050830201017] [Fixes, reworked 2nd chapter, conclusion Matthieu Sozeau **20050831010637] [Minor fixes, remove TypeType refs, use the right mu Matthieu Sozeau **20050831102329] [Fixes from christine Matthieu.Sozeau@lri.fr**20050831164035] [Remerciements et présentation des tactiques Matthieu Sozeau **20050831192809] [Page de garde Matthieu Sozeau **20050831234223] [Morning fixes Matthieu Sozeau **20050901132131] [Afternoon fixes Matthieu.Sozeau@lri.fr**20050901172427] [Final version Matthieu Sozeau **20050902104413] [Plain-url bibstyle Matthieu Sozeau **20050902104605] [Sent version Matthieu.Sozeau@lri.fr**20050902173657] [Formalized rewriting algo Matthieu Sozeau **20050903162130] [subset -> mysubset Matthieu Sozeau **20050903164124] [Trying proof with interpretation (exactly the code used), hope this will work Matthieu Sozeau **20050903174643] [Advancing substitution proof Matthieu Sozeau **20050904173026] [New slides Matthieu Sozeau **20050904203333] [Work on subst proof Matthieu Sozeau **20050905125604] [Figures with pi_1 instead of proj1_sig Matthieu.Sozeau@lri.fr**20050905165812] [Better impl presentation Matthieu.Sozeau@lri.fr**20050906150311] [Nice slides Matthieu Sozeau **20050905224222] [LRI work Matthieu.Sozeau@lri.fr**20050906152037] [Fixes from merge Matthieu.Sozeau@lri.fr**20050906152715] [Final slides Matthieu Sozeau **20050908105421] [Proof files Matthieu Sozeau **20050908105710] [Work on proof Matthieu Sozeau **20050908205657] [Use vectors instead of lists Matthieu Sozeau **20050909161218] [Finished Vector proofs Matthieu.Sozeau@lri.fr**20050911193206] [Go back to lists for coq proof, continue subst proof Matthieu.Sozeau@lri.fr**20050922101758] [New proof induction hypothesis, Var case Matthieu Sozeau **20050926084730] [Removing a concl in subst proof Matthieu.Sozeau@lri.fr**20051003093739] [Rework proof Matthieu.Sozeau@lri.fr**20051004125003] [Rework proof, nth iteration Matthieu Sozeau **20051013153230] [Cleanup Matthieu.Sozeau@lri.fr**20051014150436] [Coercion transitivity proof Matthieu.Sozeau@lri.fr**20051014181558] [New version of proof, expected simpler Matthieu.Sozeau@lri.fr**20051018154946] [Continue new proof Matthieu Sozeau **20051019115106] [Rework proof Matthieu Sozeau **20051104150934] [Transitivity of coercion proof Matthieu.Sozeau@lri.fr**20051114172353] [Transition impl proof Matthieu Sozeau **20051116142854] [Update trans proof Matthieu.Sozeau@lri.fr**20051116163152] [Better trans proof Matthieu Sozeau **20051117191815] [Forgot to add some files... Matthieu Sozeau **20051118114344] [... Matthieu Sozeau **20051125140854] [Lemma 1 and beg. of 2 done of new proof scheme Matthieu Sozeau **20051201210208] [Finished first try at the proof Matthieu Sozeau **20051206174709] [Added missing proof files Matthieu.Sozeau@lri.fr**20051207225844] [Beggining from COC Matthieu Sozeau **20051208164845] [Missing COC files Matthieu Sozeau **20051208165816] [Work on COC version Matthieu Sozeau **20051209115411] [Continue proof Matthieu Sozeau **20051210230355] [Resolve pair problem for uniqueness Matthieu Sozeau **20051211120843] [Continue proof, problem for type uniqueness Matthieu Sozeau **20051211174327] [Continue proof, problem with uniqueness Matthieu Sozeau **20051212102641] [In types, proving subject reduction Matthieu.Sozeau@lri.fr**20051212210741] [Proved basic meta-theory for ECC Matthieu Sozeau **20051213122924] [Add missing files Matthieu Sozeau **20051213170222] [Decidability of conversion proved (for sn terms) Matthieu.Sozeau@lri.fr**20051213180330] [Remove old files Matthieu.Sozeau@lri.fr**20051213182759] [Moved files Matthieu.Sozeau@lri.fr**20051213183249] [Removed old make Matthieu.Sozeau@lri.fr**20051213183406] [Reworked file hierarchy Matthieu.Sozeau@lri.fr**20051213191839] [Forgot Make file Matthieu.Sozeau@lri.fr**20051213191944] [Forgot Lift and Reduction files Matthieu.Sozeau@lri.fr**20051213192045] [Begin CCP proof Matthieu Sozeau **20051215120438] [Forgot other files Matthieu Sozeau **20051215120619] [Progress in CCP proofs Matthieu Sozeau **20051215190541] [Added env Matthieu Sozeau **20051216122526] [Work on CCP proof Matthieu Sozeau **20051220110606] [CCPD a la Chen Matthieu Sozeau **20051222120841] [Before cleaning Matthieu.Sozeau@lri.fr**20060109155831] [Some cleaning done Matthieu.Sozeau@lri.fr**20060109183431] [Updated proofs Matthieu Sozeau **20060111092124] [Work on trans proof Matthieu.Sozeau@lri.fr**20060112145613] [Advance in proof stuck at sigma Matthieu Sozeau **20060112184317] [Friday's work Matthieu.Sozeau@lri.fr**20060113185108] [Monday work Matthieu Sozeau **20060116162152] [Monday work update Matthieu Sozeau **20060116172300] [Review and li'll fixes Matthieu.Sozeau@lri.fr**20060117182459] [Wednesday work Matthieu Sozeau **20060118193038] [Work on eqb presevation proof Matthieu.Sozeau@lri.fr**20060119183134] [Friday work Matthieu.Sozeau@lri.fr**20060120174119] [Christine's corrections Matthieu Sozeau **20060130134335] [Some fixes (existentials) needs work on sorting conditions Matthieu.Sozeau@lri.fr**20060130182514] [Finish some proofs, reworked SumDep rule Matthieu Sozeau **20060131183518] [Rework defs of rules with macros, prepare for fixing algo part Matthieu.Sozeau@lri.fr**20060201172603] [Fixed most of algo part Matthieu.Sozeau@lri.fr**20060201185018] [Work on equivalence preservation Matthieu Sozeau **20060206124607] [Remove obsolete case Matthieu.Sozeau@lri.fr**20060209153155] [Finished proof for real, Champagne Matthieu Sozeau **20060213172730] [Latest fixes Matthieu Sozeau **20060214122904] [Fix mu repr Matthieu Sozeau **20060215124104] [Christine fixes Matthieu Sozeau **20060301175326] [Fix fixes, and resolve problem with sorts Matthieu.Sozeau@lri.fr**20060302162106] [Move slides to slides-master for preparing TYPES'06 slides Matthieu.Sozeau@lri.fr**20060303134047] [Beginning of TYPES'06 slides Matthieu.Sozeau@lri.fr**20060303161752] [Submitted abstract Matthieu.Sozeau@lri.fr**20060307173755] [Forgot to actually add the files Matthieu.Sozeau@lri.fr**20060308195411] [Beginning of slides Matthieu.Sozeau@lri.fr**20060315180751] [First draft of slides Matthieu.Sozeau@lri.fr**20060320181009] [Flash talk version Matthieu Sozeau **20060331162030] [Bigpic's Matthieu Sozeau **20060405083126] [Prepare for merge of slides Matthieu.Sozeau@lri.fr**20060410174436] [Updated version Matthieu Sozeau **20060411173634] [Claire- and spell-checked Matthieu Sozeau **20060411201334] [Fixes from repetition Matthieu Sozeau **20060413203206] [Fixes on new slides, still needs work on images and impl Matthieu.Sozeau@lri.fr**20060414142918] [Finished Matthieu Sozeau **20060416182614] [Final rev Matthieu Sozeau **20060417102152] [Finished (really) Matthieu Sozeau **20060417124305] [Finished (really really) Matthieu Sozeau **20060417133036] [Began the article Matthieu Sozeau **20060430234750] [Typing in Russel section Matthieu Sozeau **20060501132019] [Update outline Matthieu Sozeau **20060501132926] [Algo typing Matthieu Sozeau **20060501162608] [Typesetting fixes Matthieu Sozeau **20060501175859] [One minute fixes Matthieu Sozeau **20060502170515] [Bib fixes Matthieu Sozeau **20060503223450] [Fix environment scripts Matthieu Sozeau **20060504121921] [Bib fixes Matthieu Sozeau **20060504122641] [Remove old file Matthieu Sozeau **20060504214421] [Remove old file Matthieu.Sozeau@lri.fr**20060504134339] [Progress Matthieu.Sozeau@lri.fr**20060504173223] [Fix wf macro and add werner ref Matthieu Sozeau **20060504225211] [Much work, structural lemmas ok. Need to prove unicity of sorting before going further (inversion needs just that) Matthieu Sozeau **20060505200204] [Got to extend Gang Chen's work with Sigmas, otherwise things go well :) Matthieu Sozeau **20060506004742] [Almost got unicity of sorting, needs work on sigmas and projections Matthieu Sozeau **20060506233121] [Got unicity of sorting, restricted sum and get rid of let in Matthieu Sozeau **20060507165912] [Toward SR Matthieu Sozeau **20060508164616] [Toward SR much work needed to get the unicity of sorting for conv following gang chen, maybe another solution is envisageable Matthieu Sozeau **20060508172858] [Trying with a different presentation of the coercion judgement Matthieu Sozeau **20060509104744] [Fix bib and add new system in proof, Russell for which we have unicity of sorting Matthieu Sozeau **20060509235124] [Proved SR Matthieu Sozeau **20060510105601] [Work on transitivity proof, problem with the criterion for discriminating some derivations Matthieu.Sozeau@lri.fr**20060511184952] [Almost finished transitivity proof Matthieu.Sozeau@lri.fr**20060512181928] [Proper transitivity patch Matthieu Sozeau **20060514195830] [Defining depth on the Prop judgement Matthieu Sozeau **20060514215406] [Defined new judgement with depth, got transitivity for free Matthieu Sozeau **20060515175401] [RusselMinus and correct sorts Matthieu Sozeau **20060517093542] [Some cleanup and try range (and fail) Matthieu Sozeau **20060518101557] [Fix names of ind principles, add EJCP'06 slides Matthieu Sozeau **20060518142159] [Range won't work without unique sorts for conv. That's definitive. Almost finished updating the transitivity proof to the new sumsort (the real one) Matthieu Sozeau **20060518213414] [Recover uniqueness of sorts by removing unsafe sums Matthieu Sozeau **20060521122328] [Added TPOSR development, re-finished transitivity proof Matthieu Sozeau **20060521183236] [Removed 'let in' Matthieu Sozeau **20060521185450] [Advance in TPOSR. labels at pi's ? change lifting of app label... urgent.. Matthieu Sozeau **20060522001907] [Advance TPOSR metatheory. Have to clarify which systems we use, next is substitution, weakening et al Matthieu Sozeau **20060522100129] [Cleanup in Russell, reproved SR with Axioms Matthieu Sozeau **20060522144507] [Cleanup in Russell, using double ind Matthieu Sozeau **20060522153220] [Finished cleanup, beginning of J(udgemental equality)Russel dev Matthieu Sozeau **20060522154304] [Have to use some sort of weakening Matthieu Sozeau **20060522180814] [Add conversion module Matthieu Sozeau **20060522191343] [Refinining JRussell, beginning generation lemmas Matthieu Sozeau **20060523005610] [Basic metatheory of JRussell finished, soudness of TPOSR with respect to it too Matthieu Sozeau **20060523181554] [From JRussell to Russell done, needs transitivity only for transitivity Matthieu Sozeau **20060524014510] [Proved the corrolaries which could have needed uniqueness of types. They don't :) Matthieu Sozeau **20060524114050] [Forgot TypeCase Matthieu Sozeau **20060524141714] [params Matthieu Sozeau **20060524144257] [Metatheory of TPOSR continued Matthieu Sozeau **20060524173507] [Prepare for proofs of TPOSR, much admitted Matthieu Sozeau **20060524224550] [Fix typing notation to avoid problems with ltac. Matthieu Sozeau **20060525164536 Also distinguish between Russell (|--) and JRussell (|-=), TPOSR is no problem. Added depth-indexed TPOSR derivations, used in generation for proving validity (in progress). ] [Proved validity and functionality for TPOSR, finished with the auxiliary metatheory Matthieu Sozeau **20060525194059] [The pi labelling patch, the only way to get uniqueness of types Matthieu Sozeau **20060526010614] [In the Church-Rosser proof, at pi1, taking a break... Matthieu Sozeau **20060526195907] [Pi1 is hard, needed to change the labeling treatment to a _more_ liberal one Matthieu Sozeau **20060527014619] [Finished Pi1, at Pi2 Matthieu Sozeau **20060527111313] [Left Pi2, proved confluence and injectivity of Pi :)) Matthieu Sozeau **20060528150344] [Forgot some much important files Matthieu Sozeau **20060528151115] [Fix misuse of -R .. which maps _recursively_ Matthieu Sozeau **20060528175613] [Fix fix :) Matthieu Sozeau **20060528182819] [remove depend Matthieu Sozeau **20060528183106] [Fix new binding of 'assert by' Matthieu Sozeau **20060528194052] [Injectivity of sums... set up dev env on cocaine Matthieu Sozeau **20060528221509] [Some reworking of equiv and generation lemmas, got to adapt cr proof Matthieu Sozeau **20060529175855] [Makefiles and SR for TPOSR file Matthieu Sozeau **20060529222140] [Fix proof of CR, proved SR for beta and pi1, the rest should be easy, if tedious Matthieu Sozeau **20060529225418] [Various fixes, blocked at some substitution lemma... Matthieu Sozeau **20060531002032] [Abstract for ws on metatheory Matthieu Sozeau **20060531092712] [Add some bib, draft of abstract for ws Matthieu Sozeau **20060531104808] [Abstract sent to Christine Matthieu Sozeau **20060531105309] [Forgot to add Equiv.v Matthieu Sozeau **20060531105836] [Fix proof for doc generation Matthieu Sozeau **20060531111735] [Removed old files, better doc support Matthieu Sozeau **20060531130130] [Added notes for ICFP Matthieu Sozeau **20060531120054] [Spell-checked abstract and fix url Matthieu Sozeau **20060531131340] [More sensible dir name Matthieu Sozeau **20060531131907] [Finished UnlabConv for App (quicker) Matthieu Sozeau **20060531170138] [makedoc fixes Matthieu Sozeau **20060602165022] [li'll fixes Matthieu Sozeau **20060602100351] [Put CCSum into working form again Matthieu Sozeau **20060602181830] [Put CCSum into working form again Matthieu Sozeau **20060602181906] [TAG First checkpoint Matthieu Sozeau **20060602110517] [li'll fixes again Matthieu Sozeau **20060602171854] [Abstract sent Matthieu Sozeau **20060602182507] [Fixes from ploc Matthieu Sozeau **20060605154329] [Finisished UnlabConv proofs Matthieu Sozeau **20060608103134] [Fix on slides for EJCP Matthieu Sozeau **20060628202924] [before going to real tposr Matthieu Sozeau **20060629141653] [Done tposr -> (J)Russell translation Matthieu Sozeau **20060629153348] [Updated proofs up to cr. Need a sorts property like for Russell to get proper injectivity of sum Matthieu Sozeau **20060629231205] [Finished cr, going to sr Matthieu Sozeau **20060702124150] [Redoing transitivity for TPOSR as it is needed for SR Matthieu Sozeau **20060702163239] [Finished redoing transitivity Matthieu Sozeau **20060702185337] [New transitivity on Prop derivations Matthieu Sozeau **20060703082337] [Removed axioms for injectivity, one remaining for narrowing Matthieu Sozeau **20060703164049] [Bettering translation between coerce judgements Matthieu Sozeau **20060703171656] [Finished up until SR, proved for beta already :=) Matthieu Sozeau **20060703204422] [Problem at unlabeling, tposr is too small, need to add subtyping at app Matthieu Sozeau **20060704115732] [Passed CR with new app Matthieu Sozeau **20060704133533] [TPOSR_trans admitted, can be done with some time Matthieu Sozeau **20060705000442] [got UnlabConv app case right this time :) Matthieu Sozeau **20060705111837] [Prepared to finish metatheory Matthieu Sozeau **20060705124646] [Prove SR for Russell and JRussell Matthieu Sozeau **20060705135037] [Working on beginning proofs of TPOSR Matthieu Sozeau **20060706184724] [Working on refl and subst Matthieu Sozeau **20060707114746] [Adding substitution of a tposr deration Matthieu Sozeau **20060707115249] [Adding context coercion Matthieu Sozeau **20060707120052] [Almost got subst of TPOSR, still some thinking to do about coercion rules Matthieu Sozeau **20060707162120] [Got subst of TPOSR and Right refl yay Matthieu Sozeau **20060709121358] [Got everything for original derivations Matthieu Sozeau **20060709130113] [Got everything for a correct notion of subtyping on pi* labels Matthieu Sozeau **20060709154035] [Some reordering and renaming Matthieu Sozeau **20060710161902] [Doing proofs in CoerceNoTrans Matthieu Sozeau **20060710165928] [Forgot to add some files Matthieu Sozeau **20060710170024] [Backported changes in later proofs Matthieu Sozeau **20060710203555] [Doing generation lemmas Matthieu Sozeau **20060711142050] [Finished Generation, in ChurchRosser Matthieu Sozeau **20060711185243] [Got CRDepth for app/beta Matthieu Sozeau **20060712123037] [Almost finished CR for pi's Matthieu Sozeau **20060712172014] [Finally got completely proved SR, in unlab conv Matthieu Sozeau **20060713110126] [Need to finish unlab conv for pi's and complete TPOSR_trans Matthieu Sozeau **20060713140541] [Finished Unlab conv, still some lemmas in TPOSR_trans to do and Russell_TPOSR Matthieu Sozeau **20060713204927] [Finished complete proof of Subject Reduction Matthieu Sozeau **20060714134304] [Some notes on the proof, prove unicity of sorting in JRussell, without any axiom Matthieu Sozeau **20060715192716] [Got everything right without axioms, need to think about how to get elim of trans to Russell Matthieu Sozeau **20060715212014] [Abandon idea of getting transitivity to other systems for now, concentrate on getting Russell in good shape Matthieu Sozeau **20060716133909] [Finished proof, definitely. No axiom remain, all proofs have been done. The three systems are equivalent and have SR :) Matthieu Sozeau **20060716182854] [Update to new presentation with types in the coercion derivation judgement Matthieu Sozeau **20060716183024] [Minor paper fixes Matthieu Sozeau **20060718125614] [CP fixes Matthieu Sozeau **20060718135212] [Continue article Matthieu Sozeau **20060721174009] [First real draft of article Matthieu Sozeau **20060801151844] [Fixes, biblio Matthieu Sozeau **20060816134304] [Sorting of sub fix Matthieu Sozeau **20060816135339] [Christine Fixes, small Matthieu Sozeau **20060822124755] [Little remaining fixes Matthieu Sozeau **20060823113255] [Rework example, various nice fixes Matthieu Sozeau **20060823130115] [Bib fixes Matthieu Sozeau **20060823130642] [British spell checking, e.g. and i.e. corrections Matthieu Sozeau **20060823155527] [Last pass fixes Matthieu Sozeau **20060828142141] [Various fixes Matthieu Sozeau **20060901143316] [New notation for sub args Matthieu Sozeau **20060901141949] [Rework questionable para Matthieu Sozeau **20060901145819] [JCF fixes and more Matthieu Sozeau **20060913174000] [CPM fixes Matthieu Sozeau **20060914144745] [Submitted version Matthieu Sozeau **20060914170300] [Add russell algorithmic typing defs Matthieu Sozeau **20060928124932] [Head Normal forms Matthieu Sozeau **20060928125832] [Work on hnf Matthieu Sozeau **20061002091324] [Tries hnf Matthieu Sozeau **20061010145422] [Update proof Matthieu Sozeau **20070105171638] [Hnf proof Matthieu Sozeau **20070106150308] [Head normal form for sn terms defined, new Combined kw Matthieu Sozeau **20070106191304] [work on Hnf Matthieu Sozeau **20070108164603] [Work on Hnf Matthieu Sozeau **20070110000756] [Lambda calc with crazy dependent type Matthieu Sozeau **20070115120721] [Comment to publish hnf Matthieu Sozeau **20070123151815] [mycoqtop Matthieu Sozeau **20070123152157] [Correct typeos and some remarks Matthieu Sozeau **20070123145044] [Some more remarks rework Matthieu Sozeau **20070123152202] [New hnf Matthieu Sozeau **20070124135137] [Work on hnf Matthieu Sozeau **20070129121815] [Fixes from Christine Matthieu Sozeau **20070130171957] [Latest fixes Matthieu Sozeau **20070131111151] [Before strip for sending Matthieu Sozeau **20070131154334] [Submitted final version Matthieu Sozeau **20070131162139] [Fix order of args for hnf Matthieu Sozeau **20070203151816] [PLPV article beggining Matthieu Sozeau **20070203183909] [Prepare new slides Matthieu Sozeau **20070302143920] [Work on slides Matthieu Sozeau **20070304235554] [Little fixes Matthieu Sozeau **20070306110007] [Remove unnecessary styles, update slides Matthieu Sozeau **20070306171558] [Work on slides, corrections from Christine Matthieu Sozeau **20070307180213] [Rework conclusion and end Matthieu Sozeau **20070307202626] [Work on introduction Matthieu Sozeau **20070307222343] [Final tweaking Matthieu Sozeau **20070307230036] [Little fixes Matthieu Sozeau **20070308122256] [Fix end of ft Matthieu Sozeau **20070308133133] [Fix seq slide Matthieu Sozeau **20070308133528] [Better euclid Matthieu Sozeau **20070308141645] [ Euclid modified in real time Matthieu Sozeau **20070309160504] [Commit proval version of slides, work on Christine's fixes Matthieu Sozeau **20070312160157] [Spelling issues, fingertree example done Matthieu Sozeau **20070313203222] [Minor presentation fixes Matthieu Sozeau **20070314100734] [Fixes fron christine, finger trees form a separate section Matthieu Sozeau **20070314122537] [Finish fixes from Christine Matthieu Sozeau **20070314130455] [TYPES'07 slides directory Matthieu Sozeau **20070401144859] [Slides on Finger Trees only Matthieu Sozeau **20070401211457] [Better doc, don't put hnf in it Matthieu Sozeau **20080201054021]