2011 Archives by author

• Messages sorted by: [ thread ] [ subject ] [ date ]
• More info on this list...

Starting: Sat Jan 1 13:02:47 CEST 2011
Ending: Sat Dec 31 12:22:42 CEST 2011
Messages: 1104

• [Agda] CFP: Programming Languages meets Program Verification (PLPV 2012)   PLPV 2012
• [Agda] 2nd CFP: Programming Languages meets Program Verification (PLPV 2012)   PLPV 2012
• [Agda] Call for Contributions - Haskell Communities and Activities Report, May 2011 edition   Janis Voigtländer
• [Agda] REMINDER: Haskell Communities and Activities Report, May 2011 edition   Janis Voigtländer
• [Agda] ANNOUNCE: Haskell Communities and Activities Report (20th ed., May 2011)   Janis Voigtländer
• [Agda] Compile-time parsing   Andres Löh
• [Agda] Problem with propositional equality (or my understanding of it)   José Pedro Magalhães
• [Agda] Re: Problem with propositional equality (or my understanding of it)   José Pedro Magalhães
• [Agda] Auto   Andrés Sicard-Ramírez
• [Agda] Auto   Andrés Sicard-Ramírez
• [Agda] Auto   Andrés Sicard-Ramírez
• [Agda] code.haskell.org   Andrés Sicard-Ramírez
• [Agda] Agda's unification: postulates versus data types   Andrés Sicard-Ramírez
• [Agda] Abstract, definitional equality and propositional equality   Andrés Sicard-Ramírez
• [Agda] Abstract, definitional equality and propositional equality   Andrés Sicard-Ramírez
• [Agda] Abstract, definitional equality and propositional equality   Andrés Sicard-Ramírez
• [Agda] Binding two identifiers using user-defined syntax   Andrés Sicard-Ramírez
• [Agda] Binding two identifiers using user-defined syntax   Andrés Sicard-Ramírez
• [Agda] Binding two identifiers using user-defined syntax   Andrés Sicard-Ramírez
• [Agda] Building with GHC 7.4   Andrés Sicard-Ramírez
• [Agda] Building with GHC 7.4   Andrés Sicard-Ramírez
• [Agda] CFP WFLP 2011   Janis Voigtländer
• [Agda] Agda as an embedded language   Ertugrul Söylemez
• [Agda] FSFLA 2011: call for participation   "Carlos Martín Vide"
• [Agda] WSMBio 2012: 1st announcement   "Carlos Martín Vide"
• [Agda] PhD Positions on Trustworthy Electronic Elections   Carsten Schürmann
• [Agda] red background when trying to define the Fibonacci sequence   Andreas Abel
• [Agda] Agda Observational equality using primUnsafeTrustMe?   Andreas Abel
• [Agda] Agda standard library tutorial?   Andreas Abel
• [Agda] Agda standard library tutorial?   Andreas Abel
• [Agda] Agda standard library tutorial?   Andreas Abel
• [Agda] Extending Pattern Unification to Records   Andreas Abel
• [Agda] Yet another questions about equality   Andreas Abel
• Fwd: Re: [Agda] Yet another questions about equality   Andreas Abel
• Fwd: Re: [Agda] Yet another questions about equality   Andreas Abel
• [Agda] Yet another questions about equality   Andreas Abel
• [Agda] Yet another questions about equality   Andreas Abel
• [Agda] Yet another questions about equality   Andreas Abel
• [Agda] ANNOUNCE: Agda 2.2.10   Andreas Abel
• [Agda] ANNOUNCE: Agda 2.2.10   Andreas Abel
• Yellow irrelevant metas [Re: [Agda] Re: comlicated equivalence: need help to prove: errh, addres of repository]   Andreas Abel
• [Agda] Converting a pattern match to an equality   Andreas Abel
• [Agda] agda semantics   Andreas Abel
• [Agda] AIM XIII accomodation   Andreas Abel
• [Agda] change in handling of irrelevant parameters (bug?)   Andreas Abel
• [Agda] Record types are not allowed in mutual blocks   Andreas Abel
• [Agda] Bug in record definition   Andreas Abel
• [Agda] Irrelevance and equalities?   Andreas Abel
• [Agda] Proposed Agda feature: non-canonical implicit arguments   Andreas Abel
• [Agda] Fixing inferExpr panic   Andreas Abel
• [Agda] vector foldl Miller magic?   Andreas Abel
• [Agda] Termination Checking   Andreas Abel
• [Agda] Termination Checking   Andreas Abel
• [Agda] Unification, the yellow stuff   Andreas Abel
• [Agda] A question of terminology   Andreas Abel
• [Agda] AIM XIII code sprints   Andreas Abel
• [Agda] Is this a bug?   Andreas Abel
• [Agda] AIM XIII code sprints   Andreas Abel
• [Agda] Is this a bug?   Andreas Abel
• Parameters and indices [Re: [Agda] general question]   Andreas Abel
• Equality on Types [Re: [Agda] Is this a bug?]   Andreas Abel
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Andreas Abel
• [Agda] Re: Syntax for anonymous functions [Re: AIM XIII code sprints]   Andreas Abel
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Andreas Abel
• [Agda] Record "Setters"?   Andreas Abel
• [Agda] Record "Setters"?   Andreas Abel
• [Agda] Re: records in mutual blocks   Andreas Abel
• [Agda] Building Coinductive Trees   Andreas Abel
• [Agda] heap mistery   Andreas Abel
• [Agda] heap mistery   Andreas Abel
• [Agda] Re: Syntax for anonymous functions   Andreas Abel
• [Agda] Postulating double-negated consistent axioms without breaking canonicity?   Andreas Abel
• [Agda] Postulating double-negated consistent axioms without breaking canonicity?   Andreas Abel
• [Agda] Re: Syntax for anonymous functions   Andreas Abel
• [Agda] mutual haskell types with MAlonzo   Andreas Abel
• Broken Interaction Tests [Re: [Agda] Re: Syntax for anonymous functions]   Andreas Abel
• Broken Interaction Tests [Re: [Agda] Re: Syntax for anonymous functions]   Andreas Abel
• Broken Interaction Tests [Re: [Agda] Re: Syntax for anonymous functions]   Andreas Abel
• [Agda] Agda compiler backend targeting JavaScript   Andreas Abel
• [Agda] Sized types and coinduction   Andreas Abel
• [Agda] curious   Andreas Abel
• Study type theory in Europe [Re: [Agda] curious]   Andreas Abel
• [Agda] Impossible proofs about where blocks?   Andreas Abel
• [Agda] Impossible proofs about where blocks?   Andreas Abel
• [Agda] constructor-headed functions to Set   Andreas Abel
• [Agda] Divergence in inference with constructor-headed functions   Andreas Abel
• [Agda] Irrelevance and propositional equality   Andreas Abel
• [Agda] constructor-headed functions to Set   Andreas Abel
• [Agda] Agda performance improvements   Andreas Abel
• [Agda] Cannot type-check Level.agda in the Agda standard library with the current Agda 2.2.11 (command line)   Andreas Abel
• [Agda] Compiler internals for projection functions   Andreas Abel
• [Agda] New release soon   Andreas Abel
• [Agda] Pattern matching on irrelevant data   Andreas Abel
• [Agda] Pattern matching on irrelevant data   Andreas Abel
• [Agda] Pattern matching on irrelevant data   Andreas Abel
• [Agda] Pattern matching on irrelevant data   Andreas Abel
• [Agda] Agda's coinduction incompatible with initial algebras   Andreas Abel
• [Agda] Agda's coinduction incompatible with initial algebras   Andreas Abel
• [Agda] Agda's coinduction incompatible with initial algebras   Andreas Abel
• [Agda] Pattern matching on irrelevant data   Andreas Abel
• [Agda] Agda's coinduction incompatible with initial algebras   Andreas Abel
• [Agda] Agda's coinduction incompatible with initial algebras   Andreas Abel
• [Agda] Pattern matching on irrelevant data   Andreas Abel
• [Agda] Agda's coinduction incompatible with initial algebras   Andreas Abel
• [Agda] Read up on cabal insanities   Andreas Abel
• [Agda] Associativity for free!   Andreas Abel
• [Agda] Re: Associativity for free!   Andreas Abel
• [yoshiki] Re: [Agda] Associativity for free!   Andreas Abel
• [Agda] A proof of the irrationality of the square root in Agda   Andreas Abel
• [Agda] subset types? refinement types? type synonyms? type abbreviations?   Andreas Abel
• [Agda] collections/containers/finite sets   Andreas Abel
• [Agda] collections/containers/finite sets   Andreas Abel
• [Agda] Are there unicorns in Agda?   Andreas Abel
• Fwd: [Agda] Parallel or   Andreas Abel
• [Agda] a termination problem   Andreas Abel
• [Agda] a termination problem   Andreas Abel
• [Agda] a termination problem   Andreas Abel
• [Agda] how does BUILTIN work - practical programming in Agda   Andreas Abel
• [Agda] how does BUILTIN work - practical programming in Agda   Andreas Abel
• [Agda] Relaxing the strict positivity requirement   Andreas Abel
• gradual typing [Re: [Agda] Compile-time parsing]   Andreas Abel
• [Agda] Agda Implementors' Meeting XV: please register   Andreas Abel
• [Agda] Agda Implementors' Meeting XV: please register   Andreas Abel
• [Agda] LTL Types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs   Colin Adams
• [Agda] curious   Danel Ahman
• [Agda] Efficient numeric computations in Agda   Arseniy Alekseyev
• [Agda] Cannot type-check Level.agda in the Agda standard library with the current Agda 2.2.11 (command line)   Arseniy Alekseyev
• [Agda] A proof of the irrationality of the square root in Agda   Arseniy Alekseyev
• [Agda] interactive evaluation and typechecking   Arseniy Alekseyev
• [Agda] collections/containers/finite sets   Arseniy Alekseyev
• [Agda] collections/containers/finite sets   Arseniy Alekseyev
• [Agda] Size of propositional equality?   Thorsten Altenkirch
• [Agda] red background when trying to define the Fibonacci sequence   Thorsten Altenkirch
• [Agda] Agda Observational equality using primUnsafeTrustMe?   Thorsten Altenkirch
• [Agda] Agda Observational equality using primUnsafeTrustMe?   Thorsten Altenkirch
• [Agda] MGS 2011   Thorsten Altenkirch
• Re: [Agda] Universes à la Tarski and induction-recursion   Thorsten Altenkirch
• [Agda] Yet another questions about equality   Thorsten Altenkirch
• [Agda] Yet another questions about equality   Thorsten Altenkirch
• [Agda] Yet another questions about equality   Thorsten Altenkirch
• [Agda] Yet another questions about equality   Thorsten Altenkirch
• [Agda] Yet another questions about equality   Thorsten Altenkirch
• [Agda] Record types are not allowed in mutual blocks   Thorsten Altenkirch
• [Agda] Academic reference for the Fin data type   Thorsten Altenkirch
• [Agda] Record types are not allowed in mutual blocks   Thorsten Altenkirch
• [Agda] elements of recursive records   Thorsten Altenkirch
• [Agda] Re: elements of recursive records   Thorsten Altenkirch
• [Agda] A question of terminology   Thorsten Altenkirch
• Equality on Types [Re: [Agda] Is this a bug?]   Thorsten Altenkirch
• [Agda] Re: Syntax for anonymous functions [Re: AIM XIII code sprints]   Thorsten Altenkirch
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Thorsten Altenkirch
• [Agda] Running a classical proof with choice in Agda   Thorsten Altenkirch
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Thorsten Altenkirch
• [Agda] records in mutual blocks   Thorsten Altenkirch
• [Agda] records in mutual blocks   Thorsten Altenkirch
• [Agda] Recursive types for free?   Thorsten Altenkirch
• [Agda] dependent mutually inductive types   Thorsten Altenkirch
• [Agda] dependent mutually inductive types   Thorsten Altenkirch
• [Agda] Pattern matching on irrelevant data   Thorsten Altenkirch
• [Agda] Agda's coinduction incompatible with initial algebras   Thorsten Altenkirch
• [Agda] Agda's coinduction incompatible with initial algebras   Thorsten Altenkirch
• [Agda] Agda's coinduction incompatible with initial algebras   Thorsten Altenkirch
• [Agda] Agda's coinduction incompatible with initial algebras   Thorsten Altenkirch
• [Agda] Agda's coinduction incompatible with initial algebras   Thorsten Altenkirch
• Yoneda was Re: [Agda] Associativity for free!   Thorsten Altenkirch
• Yoneda was Re: [Agda] Associativity for free!   Thorsten Altenkirch
• [Agda] termination   Jesper Louis Andersen
• [Agda] New user question. Why does Agda reject my program.   Jesper Louis Andersen
• [Agda] Re: Agda running in the browser   Jesper Louis Andersen
• [Agda] 'Dummie' question - why records?   Jesper Louis Andersen
• [Agda] Call for Papers: Conference on Domain-Specific Languages (DSL 2011)   Emilie Balland
• [Agda] Re: Associativity for free!   Nick Benton
• [Agda] Workshop Announcement: Domains X   Ulrich Berger
• [Agda] Domains X 2011: Call for Participation   Ulrich Berger
• [Agda] MFPS First Call for Papers   Ulrich Berger
• [Agda] ITP 2012: Call for workshop proposals   Lennart Beringer
• [Agda] ITP'12: final call for workshop proposals   Lennart Beringer
• [Agda] Proving Parametricity?   Jean-Philippe Bernardy
• Re: [Agda] what is status of → ?   Jean-Philippe Bernardy
• [Agda] ANNOUNCE: Agda 2.2.10   Jean-Philippe Bernardy
• [Agda] ANNOUNCE: Agda 2.2.10   Jean-Philippe Bernardy
• [Agda] ANNOUNCE: Agda 2.2.10   Jean-Philippe Bernardy
• [Agda] ANNOUNCE: Agda 2.2.10   Jean-Philippe Bernardy
• [Agda] Automatic generation of trivial proofs   Jean-Philippe Bernardy
• [Agda] Proposed Agda feature: non-canonical implicit arguments   Jean-Philippe Bernardy
• [Agda] binder for existential quantifier   Jean-Philippe Bernardy
• [Agda] Proving _!_ is inverse of tabulate...   Jean-Philippe Bernardy
• [Agda] Small-scale reflection in Agda   Jean-Philippe Bernardy
• [Agda] Re: Syntax for anonymous functions   Jean-Philippe Bernardy
• [Agda] Syntax precedences   Jean-Philippe Bernardy
• [Agda] Re: 'Dummie' question - why records?   Jean-Philippe Bernardy
• [Agda] Do-notation with mix fix binders?   Jean-Philippe Bernardy
• [Agda] Binding two identifiers using user-defined syntax   Jean-Philippe Bernardy
• [Agda] Binding two identifiers using user-defined syntax   Jean-Philippe Bernardy
• [Agda] Pattern matching weirdness?   Jean-Philippe Bernardy
• [Agda] Lightweight free theorems   Jean-Philippe Bernardy
• [Agda] CSL'11 call for papers and workshop proposals   Marcus Aloysius Bezem
• [Agda] CSL'11 call for papers, deadline approaching   Marcus Aloysius Bezem
• [Agda] TYPES 2011 in Bergen 8 - 11 Sept: Deadline for abstracts 19 June   Marcus Aloysius Bezem
• [Agda] TYPES/CSL'11: registration open, TYPES deadline approaching   Marcus Aloysius Bezem
• [Agda] CfP: Domains X 2011   Jens Blanck
• [Agda] Call for Papers: 1st International Workshop on Rigorous Protocol Engineering (WRiPE 2011)   Edwin Brady
• [Agda] MGS 2011   Venanzio Capretta
• [Agda] Associativity for free!   Andrew Cave
• Re: [Agda] Universes à la Tarski and induction-recursion   James Chapman
• Fwd: Re: [Agda] Yet another questions about equality   James Chapman
• [Agda] SPLST 2011 - Call for Papers   James Chapman
• [Agda] Deadline extension: (August 31): SPLST'11   James Chapman
• [Agda] MSFP 2012: Call for Papers   James Chapman
• [Agda] New release soon   James Chapman
• [Agda] 'Dummie' question - why records?   James Chapman
• [Agda] Associativity for free!   James Chapman
• [Agda] Associativity for free!   James Chapman
• [Agda] Associativity for free!   James Chapman
• [Agda] Associativity for free!   James Chapman
• [Agda] Re: Associativity for free!   James Chapman
• [Agda] Associativity for free!   James Chapman
• [Agda] Re: Associativity for free!   James Chapman
• [Agda] Re: Associativity for free!   James Chapman
• [Agda] MSFP 2012: Second Call for Papers   James Chapman
• [Agda] MSFP 2012 deadline extension   James Chapman
• [Agda] Jobs combining type theory and web programming   Adam Chlipala
• [Agda] Hello World   Ben Clifford
• [Agda] segmentation fault when printing a number   Ben Clifford
• [Agda] July 18-21, 2011, Int'l Conf. on Image Processing, Computer Vision, & Pattern Recognition (IPCV), USA, paper submission deadline: March 10, 2011   WORLDCOMP'11 Congress Conferences
• [Agda] July 18-21, 2011, Call For Papers - PDPTA Int'l Conf. (Parallel & Distributed Processing Techniques & Applications), USA, paper submission deadline: March 10, 2011   WORLDCOMP'11 Congress Conferences
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Thierry Coquand
• [Agda] Parsing Mixfix Operators, source code?   Jason Dagit
• [Agda] Cannot type-check Level.agda in the Agda standard library with the current Agda 2.2.11 (command line)   IKEGAMI Daisuke
• [Agda] Cannot type-check Level.agda in the Agda standard library with the current Agda 2.2.11 (command line)   IKEGAMI Daisuke
• [Agda] A proof of the irrationality of the square root in Agda   IKEGAMI Daisuke
• [Agda] A proof of the irrationality of the square root in Agda   IKEGAMI Daisuke
• [Agda] A proof of the irrationality of the square root in Agda   IKEGAMI Daisuke
• [Agda] A proof of the irrationality of the square root in Agda   IKEGAMI Daisuke
• [Agda] generative thunk?   Nils Anders Danielsson
• [Agda] Tricks to limit the memory consumption?   Nils Anders Danielsson
• [Agda] Auto   Nils Anders Danielsson
• [Agda] Tricks to limit the memory consumption?   Nils Anders Danielsson
• [Agda] Agda standard library tutorial?   Nils Anders Danielsson
• [Agda] Universe construction   Nils Anders Danielsson
• [Agda] Agda standard library tutorial?   Nils Anders Danielsson
• [Agda] new release   Nils Anders Danielsson
• [Agda] --without-K   Nils Anders Danielsson
• [Agda] interactive mode   Nils Anders Danielsson
• [Agda] Problem when getting the Standard Library   Nils Anders Danielsson
• [Agda] Re: Problem when getting the Standard Library   Nils Anders Danielsson
• [Agda] Re: Problem when getting the Standard Library   Nils Anders Danielsson
• [Agda] Agda Implementors' Meeting XIII   Nils Anders Danielsson
• [Agda] repository of Agda code/proofs   Nils Anders Danielsson
• [Agda] how to count 0..n-1   Nils Anders Danielsson
• [Agda] commutativity/associativity representation   Nils Anders Danielsson
• Fwd: Re: [Agda] commutativity/associativity representation   Nils Anders Danielsson
• [Agda] what is status of → ?   Nils Anders Danielsson
• [Agda] how to count 0..n-1   Nils Anders Danielsson
• [Agda] how to count 0..n-1   Nils Anders Danielsson
• [Agda] how to count 0..n-1   Nils Anders Danielsson
• [Agda] how to count 0..n-1   Nils Anders Danielsson
• [Agda] Setoids   Nils Anders Danielsson
• [Agda] how to count 0..n-1   Nils Anders Danielsson
• [Agda] ANNOUNCE: Agda 2.2.10   Nils Anders Danielsson
• [Agda] ANNOUNCE: Standard library version 0.5   Nils Anders Danielsson
• [Agda] _ synthax   Nils Anders Danielsson
• [Agda] Re: comlicated equivalence: need help to prove: errh, addres of repository   Nils Anders Danielsson
• [Agda] lhs2tex and agda identifiers   Nils Anders Danielsson
• [Agda] agda semantics   Nils Anders Danielsson
• [Agda] Termination not being proven   Nils Anders Danielsson
• [Agda] lhs2tex and agda identifiers   Nils Anders Danielsson
• [Agda] Termination not being proven   Nils Anders Danielsson
• [Agda] refuting with rewrite   Nils Anders Danielsson
• [Agda] change in handling of irrelevant parameters (bug?)   Nils Anders Danielsson
• [Agda] Coinductive indices   Nils Anders Danielsson
• [Agda] Defining subtraction for naturals   Nils Anders Danielsson
• [Agda] Record types are not allowed in mutual blocks   Nils Anders Danielsson
• [Agda] RE: agda coredump   Nils Anders Danielsson
• [Agda] Install failure   Nils Anders Danielsson
• [Agda] Avoiding implicit argument proliferation?   Nils Anders Danielsson
• [Agda] Bug in record definition   Nils Anders Danielsson
• [Agda] Avoiding implicit argument proliferation?   Nils Anders Danielsson
• [Agda] Re: elements of recursive records   Nils Anders Danielsson
• [Agda] Avoiding implicit argument proliferation?   Nils Anders Danielsson
• [Agda] Irrelevance and equalities?   Nils Anders Danielsson
• [Agda] Proposed Agda feature: non-canonical implicit arguments   Nils Anders Danielsson
• [Agda] New user question. Why does Agda reject my program.   Nils Anders Danielsson
• [Agda] binder for existential quantifier   Nils Anders Danielsson
• [Agda] binder for existential quantifier   Nils Anders Danielsson
• [Agda] Parsing Mixfix Operators, source code?   Nils Anders Danielsson
• [Agda] Parsing Mixfix Operators, source code?   Nils Anders Danielsson
• [Agda] Is this a bug?   Nils Anders Danielsson
• [Agda] agda syb 0.3 haskell platform 2011.2.0.1   Nils Anders Danielsson
• [Agda] Is this a bug?   Nils Anders Danielsson
• Equality on Types [Re: [Agda] Is this a bug?]   Nils Anders Danielsson
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Nils Anders Danielsson
• [Agda] Instance arguments: three more updates   Nils Anders Danielsson
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Nils Anders Danielsson
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Nils Anders Danielsson
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Nils Anders Danielsson
• [Agda] Re: Syntax for anonymous functions [Re: AIM XIII code sprints]   Nils Anders Danielsson
• [Agda] Running a classical proof with choice in Agda   Nils Anders Danielsson
• [Agda] Lightweight dependency management using make   Nils Anders Danielsson
• [Agda] Re: Syntax for anonymous functions   Nils Anders Danielsson
• [Agda] Building Coinductive Trees   Nils Anders Danielsson
• [Agda] Postulating double-negated consistent axioms without breaking canonicity?   Nils Anders Danielsson
• [Agda] Postulating double-negated consistent axioms without breaking canonicity?   Nils Anders Danielsson
• [Agda] ANN: coq-like agda-mode support for databases of lemmas   Nils Anders Danielsson
• [Agda] ANN: coq-like agda-mode support for databases of lemmas - important bugfix   Nils Anders Danielsson
• [Agda] ANN: coq-like agda-mode support for databases of lemmas   Nils Anders Danielsson
• [Agda] ANN: coq-like agda-mode support for databases of lemmas   Nils Anders Danielsson
• Broken Interaction Tests [Re: [Agda] Re: Syntax for anonymous functions]   Nils Anders Danielsson
• Broken Interaction Tests [Re: [Agda] Re: Syntax for anonymous functions]   Nils Anders Danielsson
• [Agda] Typechecking failure for Agda Standard Library   Nils Anders Danielsson
• [Agda] Agda compiler backend targeting JavaScript   Nils Anders Danielsson
• [Agda] Process: how to extend the Agda standard library?   Nils Anders Danielsson
• [Agda] literate Agda with unicode in latex   Nils Anders Danielsson
• [Agda] Impossible proofs about where blocks?   Nils Anders Danielsson
• [Agda] Overlapping patterns in function definition -- strange behavior   Nils Anders Danielsson
• [Agda] ANN: agda-move-improvements-0.3   Nils Anders Danielsson
• [Agda] Syntax precedences   Nils Anders Danielsson
• [Agda] Overloaded literals   Nils Anders Danielsson
• [Agda] Absurd lambdas and equality   Nils Anders Danielsson
• [Agda] Divergence in inference with constructor-headed functions   Nils Anders Danielsson
• [Agda] constructor-headed functions to Set   Nils Anders Danielsson
• [Agda] Eta reduction of a function argument in a where block   Nils Anders Danielsson
• [Agda] Hello World   Nils Anders Danielsson
• [Agda] Irrelevance and propositional equality   Nils Anders Danielsson
• [Agda] Eta reduction of a function argument in a where block   Nils Anders Danielsson
• [Agda] hello, I've done something terrible...   Nils Anders Danielsson
• [Agda] Documentation of the (not only) latest features   Nils Anders Danielsson
• [Agda] Abstract, definitional equality and propositional equality   Nils Anders Danielsson
• [Agda] Abstract, definitional equality and propositional equality   Nils Anders Danielsson
• [Agda] Agda without emacs?   Nils Anders Danielsson
• [Agda] segmentation fault when printing a number   Nils Anders Danielsson
• [Agda] Efficient numeric computations in Agda   Nils Anders Danielsson
• [Agda] Agda without emacs?   Nils Anders Danielsson
• [Agda] Termination checking with partiality monad   Nils Anders Danielsson
• [Agda] Agda performance improvements   Nils Anders Danielsson
• [Agda] New release soon   Nils Anders Danielsson
• [Agda] Termination and efficiency of higher order functions over nested datatypes   Nils Anders Danielsson
• [Agda] New release soon   Nils Anders Danielsson
• [Agda] Unit testing   Nils Anders Danielsson
• [Agda] Agda's coinduction incompatible with initial algebras   Nils Anders Danielsson
• [Agda] Unit testing   Nils Anders Danielsson
• [Agda] Agda's coinduction incompatible with initial algebras   Nils Anders Danielsson
• [Agda] Agda's coinduction incompatible with initial algebras   Nils Anders Danielsson
• [Agda] Agda's coinduction incompatible with initial algebras   Nils Anders Danielsson
• [Agda] Agda's coinduction incompatible with initial algebras   Nils Anders Danielsson
• [Agda] Something like type classes in Agda?   Nils Anders Danielsson
• [Agda] 'Dummie' question - why records?   Nils Anders Danielsson
• [Agda] 'Dummie' question - why records?   Nils Anders Danielsson
• [Agda] Externally vs internally consistent exensions of Agda   Nils Anders Danielsson
• [Agda] 'Dummie' question - why records?   Nils Anders Danielsson
• [Agda] 'Dummie' question - why records?   Nils Anders Danielsson
• [Agda] Do-notation with mix fix binders?   Nils Anders Danielsson
• [Agda] Associativity for free!   Nils Anders Danielsson
• [Agda] Associativity for free!   Nils Anders Danielsson
• [Agda] A proof of the irrationality of the square root in Agda   Nils Anders Danielsson
• [Agda] Re: Associativity for free!   Nils Anders Danielsson
• [Agda] A proof of the irrationality of the square root in Agda   Nils Anders Danielsson
• [Agda] subset types? refinement types? type synonyms? type abbreviations?   Nils Anders Danielsson
• [Agda] Are there unicorns in Agda?   Nils Anders Danielsson
• [Agda] collections/containers/finite sets   Nils Anders Danielsson
• [Agda] collections/containers/finite sets   Nils Anders Danielsson
• [Agda] collections/containers/finite sets   Nils Anders Danielsson
• [Agda] Transitive-on   Nils Anders Danielsson
• [Agda] Transitive-on   Nils Anders Danielsson
• [Agda] interactive evaluation and typechecking   Nils Anders Danielsson
• Fwd: [Agda] Parallel or   Nils Anders Danielsson
• Fwd: [Agda] Parallel or   Nils Anders Danielsson
• [Agda] Re: strict total order on characters   Nils Anders Danielsson
• [Agda] strict total order on characters   Nils Anders Danielsson
• [Agda] implicit arguments and mixfix   Nils Anders Danielsson
• [Agda] how does BUILTIN work - practical programming in Agda   Nils Anders Danielsson
• [Agda] how does BUILTIN work - practical programming in Agda   Nils Anders Danielsson
• [Agda] type checker   Nils Anders Danielsson
• [Agda] how does BUILTIN work - practical programming in Agda   Nils Anders Danielsson
• [Agda] how does BUILTIN work - practical programming in Agda   Nils Anders Danielsson
• [Agda] how does BUILTIN work - practical programming in Agda   Nils Anders Danielsson
• [Agda] how does BUILTIN work - practical programming in Agda   Nils Anders Danielsson
• [Agda] injectivity of Data.Char.toNat?   Nils Anders Danielsson
• [Agda] Re: records and modules   Nils Anders Danielsson
• [Agda] how does BUILTIN work - practical programming in Agda   Nils Anders Danielsson
• [Agda] links in generated html files   Nils Anders Danielsson
• [Agda] Compile-time parsing   Nils Anders Danielsson
• [Agda] Compile-time parsing   Nils Anders Danielsson
• [Agda] Compile-time parsing   Nils Anders Danielsson
• [Agda] Compile-time parsing   Nils Anders Danielsson
• [Agda] Building with GHC 7.4   Nils Anders Danielsson
• [Agda] Agda as an embedded language   Nils Anders Danielsson
• [Agda] ANNOUNCE: Standard library version 0.6   Nils Anders Danielsson
• [Agda] Building with GHC 7.4   Nils Anders Danielsson
• [Agda] Building with GHC 7.4   Nils Anders Danielsson
• [Agda] Agda Observational equality using primUnsafeTrustMe?   Dominique Devriese
• [Agda] Agda Observational equality using primUnsafeTrustMe?   Dominique Devriese
• [Agda] Unsolved metas   Dominique Devriese
• [Agda] commutativity/associativity representation   Dominique Devriese
• [Agda] how to count 0..n-1   Dominique Devriese
• [Agda] Yet another questions about equality   Dominique Devriese
• [Agda] how to count 0..n-1   Dominique Devriese
• [Agda] how to count 0..n-1   Dominique Devriese
• [Agda] Proposed Agda feature: non-canonical implicit arguments   Dominique Devriese
• [Agda] Proposed Agda feature: non-canonical implicit arguments   Dominique Devriese
• [Agda] Agda faster with GHC 7   Dominique Devriese
• [Agda] Re: Agda faster with GHC 7   Dominique Devriese
• [Agda] A question of terminology   Dominique Devriese
• [Agda] A question of terminology   Dominique Devriese
• [Agda] general question   Dominique Devriese
• [Agda] general question   Dominique Devriese
• [Agda] Instance arguments: three more updates   Dominique Devriese
• [Agda] Re: Instance arguments: three more updates   Dominique Devriese
• [Agda] Instance arguments: three more updates   Dominique Devriese
• Broken Interaction Tests [Re: [Agda] Re: Syntax for anonymous functions]   Dominique Devriese
• [Agda] Syntax precedences   Dominique Devriese
• [Agda] Syntax precedences   Dominique Devriese
• [Agda] Overloaded literals   Dominique Devriese
• [Agda] Overloaded literals   Dominique Devriese
• [Agda] Hello World   Dominique Devriese
• [Agda] Do-notation with mix fix binders?   Dominique Devriese
• [Agda] collections/containers/finite sets   Dominique Devriese
• [Agda] collections/containers/finite sets   Dominique Devriese
• [Agda] Agda 2.3.0 released   Dominique Devriese
• [Agda] Compile-time parsing   Dominique Devriese
• [Agda] Agda Observational equality using primUnsafeTrustMe?   Dan Doel
• [Agda] Universe construction   Dan Doel
• [Agda] Universes à la Tarski and induction-recursion   Dan Doel
• [Agda] Universes à la Tarski and induction-recursion   Dan Doel
• [Agda] Yet another questions about equality   Dan Doel
• [Agda] ANNOUNCE: Agda 2.2.10   Dan Doel
• [Agda] ANNOUNCE: Agda 2.2.10   Dan Doel
• [Agda] ANNOUNCE: Agda 2.2.10   Dan Doel
• [Agda] Yet another questions about equality   Dan Doel
• [Agda] Coinductive indices   Dan Doel
• [Agda] Defining subtraction for naturals   Dan Doel
• [Agda] Irrelevance and equalities?   Dan Doel
• [Agda] Recursive types for free?   Dan Doel
• [Agda] Recursive types for free?   Dan Doel
• [Agda] dependent mutually inductive types   Dan Doel
• [Agda] Pattern matching on irrelevant data   Dan Doel
• [Agda] Pattern matching on irrelevant data   Dan Doel
• [Agda] Agda's coinduction incompatible with initial algebras   Dan Doel
• [Agda] Pattern matching on irrelevant data   Dan Doel
• [Agda] Agda's coinduction incompatible with initial algebras   Dan Doel
• [Agda] Agda's coinduction incompatible with initial algebras   Dan Doel
• [Agda] Agda's coinduction incompatible with initial algebras   Dan Doel
• [Agda] Agda's coinduction incompatible with initial algebras   Dan Doel
• [Agda] Agda's coinduction incompatible with initial algebras   Dan Doel
• [Agda] Are there unicorns in Agda?   Dan Doel
• Fwd: [Agda] Parallel or   Dan Doel
• Fwd: [Agda] Parallel or   Dan Doel
• [Agda] how to count 0..n-1   Jason Dusek
• [Agda] how to count 0..n-1   Jason Dusek
• [Agda] how to count 0..n-1   Jason Dusek
• [Agda] how to count 0..n-1   Jason Dusek
• [Agda] how to count 0..n-1   Jason Dusek
• [Agda] Proving _!_ is inverse of tabulate...   Jason Dusek
• [Agda] Proving _!_ is inverse of tabulate...   Jason Dusek
• [Agda] Proving _!_ is inverse of tabulate...   Jason Dusek
• [Agda] Proving _!_ is inverse of tabulate...   Jason Dusek
• RE: [Agda] Universes à la Tarski and induction-recursion   Peter Dybjer
• RE: [Agda] Universes à la Tarski and induction-recursion   Peter Dybjer
• [Agda] general question   Peter Dybjer
• [Agda] 'Dummie' question - why records?   Peter Dybjer
• [Agda] 'Dummie' question - why records?   Peter Dybjer
• [Agda] Associativity for free!   Peter Dybjer
• [Agda] Normalization by Evaluation   Peter Dybjer
• [Agda] Tricks to limit the memory consumption?   gallais at EnsL.org
• [Agda] Agda standard library tutorial?   gallais at EnsL.org
• [Agda] how to count 0..n-1   gallais at EnsL.org
• [Agda] Termination not being proven   gallais at EnsL.org
• [Agda] refuting with rewrite   gallais at EnsL.org
• [Agda] Defining subtraction for naturals   gallais at EnsL.org
• [Agda] Install failure   gallais at EnsL.org
• [Agda] Install failure   gallais at EnsL.org
• [Agda] Install failure   gallais at EnsL.org
• [Agda] Install failure   gallais at EnsL.org
• [Agda] Install failure   gallais at EnsL.org
• [Agda] Install failure   gallais at EnsL.org
• [Agda] Install failure   gallais at EnsL.org
• [Agda] Install failure   gallais at EnsL.org
• [Agda] Defining subtraction for naturals   Martin Escardo
• [Agda] Install failure   Martin Escardo
• [Agda] Install failure   Martin Escardo
• [Agda] Install failure   Martin Escardo
• [Agda] binder for existential quantifier   Martin Escardo
• [Agda] binder for existential quantifier   Martin Escardo
• [Agda] general question   Martin Escardo
• [Agda] general question   Martin Escardo
• [Agda] general question   Martin Escardo
• [Agda] general question   Martin Escardo
• [Agda] Running a classical proof with choice in Agda   Martin Escardo
• [Agda] Running a classical proof with choice in Agda   Martin Escardo
• [Agda] Running a classical proof with choice in Agda   Martin Escardo
• [Agda] Running a classical proof with choice in Agda   Martin Escardo
• [Agda] heap mistery   Martin Escardo
• [Agda] heap mistery   Martin Escardo
• [Agda] Nice programming challenge   Martin Escardo
• [Agda] Nice programming challenge   Martin Escardo
• [Agda] Nice programming challenge   Martin Escardo
• [Agda] literate Agda with unicode in latex   Martin Escardo
• [Agda] Agda performance improvements   Martin Escardo
• [Agda] A proof of omniscience in Agda   Martin Escardo
• [Agda] A proof of omniscience in Agda   Martin Escardo
• [Agda] Agda's coinduction incompatible with initial algebras   Martin Escardo
• [Agda] Agda's coinduction incompatible with initial algebras   Martin Escardo
• [Agda] Agda's coinduction incompatible with initial algebras   Martin Escardo
• [Agda] Ordinals in Agda   Martin Escardo
• [Agda] Are there unicorns in Agda?   Martin Escardo
• [Agda] Are there unicorns in Agda?   Martin Escardo
• [Agda] Are there unicorns in Agda?   Martin Escardo
• [Agda] Are there unicorns in Agda?   Martin Escardo
• [Agda] Are two equal things the same?   Martin Escardo
• [Agda] Are two equal things the same?   Martin Escardo
• [Agda] Building with GHC 7.4   Martin Escardo
• [Agda] Building with GHC 7.4   Martin Escardo
• [Agda] Building with GHC 7.4   Martin Escardo
• [Agda] new release   Permjacov Evgeniy
• [Agda] code.haskell.org   Permjacov Evgeniy
• [Agda] Unsolved metas   Permjacov Evgeniy
• Fwd: Re: [Agda] Unsolved metas   Permjacov Evgeniy
• [Agda] commutativity/associativity representation   Permjacov Evgeniy
• Fwd: Re: [Agda] commutativity/associativity representation   Permjacov Evgeniy
• [Agda] commutativity/associativity representation   Permjacov Evgeniy
• [Agda] what is status of → ?   Permjacov Evgeniy
• [Agda] Yet another questions about equality   Permjacov Evgeniy
• Fwd: Re: [Agda] Yet another questions about equality   Permjacov Evgeniy
• Fwd: Re: [Agda] Yet another questions about equality   Permjacov Evgeniy
• Fwd: Re: [Agda] Yet another questions about equality   Permjacov Evgeniy
• [Agda] Yet another questions about equality   Permjacov Evgeniy
• [Agda] Yet another questions about equality   Permjacov Evgeniy
• [Agda] Setoids   Permjacov Evgeniy
• [Agda] Applicative with arbitrary morphisms : how ?   Permjacov Evgeniy
• [Agda] _ synthax   Permjacov Evgeniy
• [Agda] comlicated equivalence: need help to prove   Permjacov Evgeniy
• [Agda] Re: comlicated equivalence: need help to prove: errh, addres of repository   Permjacov Evgeniy
• [Agda] Re: comlicated equivalence: need help to prove   Permjacov Evgeniy
• [Agda] agda semantics   Permjacov Evgeniy
• [Agda] termination   Permjacov Evgeniy
• [Agda] termination   Permjacov Evgeniy
• [Agda] termination   Permjacov Evgeniy
• [Agda] termination   Permjacov Evgeniy
• [Agda] ITP 2012: Call for Papers   Amy Felty
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Fredrik Nordvall Forsberg
• [Agda] Re: Syntax for anonymous functions   Fredrik Nordvall Forsberg
• [Agda] Re: Syntax for anonymous functions   Fredrik Nordvall Forsberg
• [Agda] CFP: DBPL '11   Nate Foster
• [Agda] DBPL '11 Call for participation   Nate Foster
• [Agda] Implicit variables on data constructors   Simon Foster
• [Agda] Implicit variables on data constructors   Simon Foster
• [Agda] Fwd: Course: Introduction to Dependently Typed Programming using Agda   Joseph Fredette
• [Agda] curious   Silvio Frischknecht
• [Agda] how does BUILTIN work - practical programming in Agda   Silvio Frischknecht
• [Agda] how does BUILTIN work - practical programming in Agda   Silvio Frischknecht
• [Agda] how does BUILTIN work - practical programming in Agda   Silvio Frischknecht
• [Agda] WSMBio 2012: 2nd announcement   GRLMC
• [Agda] WSLST 2012: 3rd announcement   GRLMC
• [Agda] SSFLA 2012: 1st announcement   GRLMC
• [Agda] WSMBio 2012: 3rd announcement   GRLMC
• [Agda] Oregon Programming Languages Summer School 2011 - Call For Participation   Marco Gaboardi
• [Agda] RTA 2012: First Call For Papers   Georg
• [Agda] Microsoft PhD Studentship   Dan Ghica
• [Agda] agda coredump   Sivaram Gowkanapalli
• [Agda] agda coredump   Sivaram Gowkanapalli
• [Agda] agda coredump   Sivaram Gowkanapalli
• [Agda] RE: agda coredump   Sivaram Gowkanapalli
• [Agda] RE: agda coredump   Sivaram Gowkanapalli
• [Agda] Bug in record definition   Sivaram Gowkanapalli
• [Agda] Agda features/functionality that I can use   Sivaram Gowkanapalli
• [Agda] Is this a bug?   Sivaram Gowkanapalli
• [Agda] FRP implementation in Agda   Robin Green
• [Agda] Efficient numeric computations in Agda   Daniel Gustafsson
• [Agda] Universe construction   David Haguenauer
• [Agda] Universe construction   David Haguenauer
• [Agda] Fixing inferExpr panic   David Haguenauer
• [Agda] Fixing inferExpr panic   David Haguenauer
• [Agda] Fixing inferExpr panic   David Haguenauer
• [Agda] Yet another questions about equality   Peter Hancock
• [Agda] Yet another questions about equality   Peter Hancock
• [Agda] Yet another questions about equality   Peter Hancock
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Peter Hancock
• [Agda] dependent mutually inductive types   Peter Hancock
• [Agda] A proof of omniscience in Agda   Peter Hancock
• [Agda] Agda's coinduction incompatible with initial algebras   Peter Hancock
• [Agda] Agda's coinduction incompatible with initial algebras   Peter Hancock
• [Agda] Choice sequences and effects   Peter Hancock
• [Agda] 'Dummie' question - why records?   Peter Hancock
• [Agda] 'Dummie' question - why records?   Peter Hancock
• [yoshiki] Re: [Agda] Associativity for free!   Peter Hancock
• [Agda] LTL Types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs   Peter Hancock
• [Agda] Relaxing the strict positivity requirement   Peter Hancock
• [Agda] Building with GHC 7.4   Peter Hancock
• [Agda] An agsy-mmetry proof   Sebastian Hanowski
• [Agda] Announcement: workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012)   Hugo Herbelin
• [Agda] Unsolved metas   Christoph Herrmann
• [Agda] Automatic generation of trivial proofs   Christoph Herrmann
• [Agda] Install failure   Christoph Herrmann
• [Agda] Install failure   Christoph Herrmann
• [Agda] Install failure   Christoph Herrmann
• [Agda] Install failure   Christoph Herrmann
• [Agda] Install failure   Christoph Herrmann
• [Agda] Install failure ghc-7.0.2 / cabal solved   Christoph Herrmann
• [Agda] Install failure ghc-7.0.2 / cabal solved   Christoph Herrmann
• [Agda] Process: how to extend the Agda standard library?   Christoph Herrmann
• [Agda] Agda without emacs?   Christoph Herrmann
• [Agda] Problem with a simple proof   Caylee Hogg
• [Agda] Problem with a simple proof   Caylee Hogg
• [Agda] Pattern matching weirdness?   Pierre Hyvernat
• [Agda] Pattern matching weirdness?   Pierre Hyvernat
• [Agda] agda semantics   Darius Jahandarie
• [Agda] Agda compiler backend targeting JavaScript   Darius Jahandarie
• [Agda] Chalmers FP is hiring 2 Assistant Professors in Functional Programming: deadline 2011-10-18   Patrik Jansson
• [Agda] ANN: coq-like agda-mode support for databases of lemmas   Wojciech Jedynak
• [Agda] ANN: coq-like agda-mode support for databases of lemmas [fixed?]   Wojciech Jedynak
• [Agda] ANN: coq-like agda-mode support for databases of lemmas - important bugfix   Wojciech Jedynak
• [Agda] ANN: coq-like agda-mode support for databases of lemmas   Wojciech Jedynak
• [Agda] ANN: coq-like agda-mode support for databases of lemmas   Wojciech Jedynak
• [Agda] ANN: convenient way to add a with expression from a goal   Wojciech Jedynak
• [Agda] ANN: agda-move-improvements-0.3   Wojciech Jedynak
• [Agda] Overlapping patterns in function definition -- strange behavior   Wojciech Jedynak
• [Agda] Re: Overlapping patterns in function definition -- strange behavior [more examples]   Wojciech Jedynak
• [Agda] Documentation of the (not only) latest features   Wojciech Jedynak
• [Agda] Eta reduction of a function argument in a where block   Wojciech Jedynak
• [Agda] Eta reduction of a function argument in a where block   Wojciech Jedynak
• [Agda] 'Dummie' question - why records?   Wojciech Jedynak
• [Agda] interactive evaluation and typechecking   Wojciech Jedynak
• [Agda] keywords, syntax   Wojciech Jedynak
• [Agda] links in generated html files   Wojciech Jedynak
• [Agda] links in generated html files   Wojciech Jedynak
• [Agda] Compile-time parsing   Wojciech Jedynak
• [Agda] Pattern matching weirdness?   Wojciech Jedynak
• [Agda] Proving Parametricity?   Alan Jeffrey
• [Agda] Proving Parametricity?   Alan Jeffrey
• [Agda] Passing numerics to haskell   Alan Jeffrey
• [Agda] Semantic Web library   Alan Jeffrey
• [Agda] Lightweight dependency management using make   Alan Jeffrey
• [Agda] Lightweight dependency management using make   Alan Jeffrey
• [Agda] Agda compiler backend targeting JavaScript   Alan Jeffrey
• [Agda] Agda compiler backend targeting JavaScript   Alan Jeffrey
• [Agda] Agda compiler backend targeting JavaScript   Alan Jeffrey
• [Agda] Agda compiler backend targeting JavaScript   Alan Jeffrey
• [Agda] Agda compiler backend targeting JavaScript   Alan Jeffrey
• [Agda] Agda compiler backend targeting JavaScript   Alan Jeffrey
• [Agda] Process: how to extend the Agda standard library?   Alan Jeffrey
• [Agda] Agda compiler backend targeting JavaScript   Alan Jeffrey
• [Agda] Overlapping patterns in function definition -- strange behavior   Alan Jeffrey
• [Agda] Two papers using Agda   Alan Jeffrey
• [Agda] Irrelevance and propositional equality   Alan Jeffrey
• [Agda] Irrelevance and propositional equality   Alan Jeffrey
• [Agda] FRP implementation in Agda   Alan Jeffrey
• [Agda] FRP implementation in Agda   Alan Jeffrey
• [Agda] Agda's unification: postulates versus data types   Alan Jeffrey
• [Agda] Efficient numeric computations in Agda   Alan Jeffrey
• [Agda] Agda running in the browser   Alan Jeffrey
• [Agda] Re: Agda running in the browser   Alan Jeffrey
• [Agda] Re: Agda running in the browser   Alan Jeffrey
• [Agda] Re: Agda running in the browser   Alan Jeffrey
• [Agda] Compiler internals for projection functions   Alan Jeffrey
• [Agda] Compiler internals for projection functions   Alan Jeffrey
• [Agda] Termination and efficiency of higher order functions over nested datatypes   Alan Jeffrey
• [Agda] Termination and efficiency of higher order functions over nested datatypes   Alan Jeffrey
• [Agda] Mapping QNames to module names?   Alan Jeffrey
• [Agda] Mapping QNames to module names?   Alan Jeffrey
• [Agda] Unit testing   Alan Jeffrey
• [Agda] Mapping QNames to module names?   Alan Jeffrey
• [Agda] Mapping QNames to module names?   Alan Jeffrey
• [Agda] Unit testing   Alan Jeffrey
• [Agda] Mapping QNames to module names?   Alan Jeffrey
• [Agda] Compiler internals for projection functions   Alan Jeffrey
• [Agda] Agda bindings for raw JS arrays and objects   Alan Jeffrey
• [Agda] Choice sequences and effects   Alan Jeffrey
• [Agda] Externally vs internally consistent exensions of Agda   Alan Jeffrey
• [Agda] 'Dummie' question - why records?   Alan Jeffrey
• [Agda] Externally vs internally consistent exensions of Agda   Alan Jeffrey
• [Agda] Associativity for free!   Alan Jeffrey
• [Agda] Associativity for free!   Alan Jeffrey
• [Agda] Associativity for free!   Alan Jeffrey
• [Agda] Associativity for free!   Alan Jeffrey
• [Agda] Associativity for free!   Alan Jeffrey
• [Agda] Associativity for free!   Alan Jeffrey
• [Agda] Associativity for free!   Alan Jeffrey
• [Agda] Re: Associativity for free!   Alan Jeffrey
• [Agda] Re: Associativity for free!   Alan Jeffrey
• [Agda] Re: Associativity for free!   Alan Jeffrey
• [Agda] Associativity for free!   Alan Jeffrey
• [Agda] Re: Associativity for free!   Alan Jeffrey
• [Agda] Re: Associativity for free!   Alan Jeffrey
• [Agda] Re: Associativity for free!   Alan Jeffrey
• [Agda] LTL Types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs   Alan Jeffrey
• [Agda] LTL Types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs   Alan Jeffrey
• [Agda] LTL Types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs   Alan Jeffrey
• [Agda] LTL Types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs   Alan Jeffrey
• [Agda] Parallel or   Alan Jeffrey
• Fwd: [Agda] Parallel or   Alan Jeffrey
• Fwd: [Agda] Parallel or   Alan Jeffrey
• Fwd: [Agda] Parallel or   Alan Jeffrey
• [Agda] Re: Associativity for free!   Alan Jeffrey
• [Agda] how does BUILTIN work - practical programming in Agda   Alan Jeffrey
• [Agda] how does BUILTIN work - practical programming in Agda   Alan Jeffrey
• [Agda] how does BUILTIN work - practical programming in Agda   Alan Jeffrey
• [Agda] how does BUILTIN work - practical programming in Agda   Alan Jeffrey
• [Agda] how does BUILTIN work - practical programming in Agda   Alan Jeffrey
• [Agda] how does BUILTIN work - practical programming in Agda   Alan Jeffrey
• [Agda] how does BUILTIN work - practical programming in Agda   Alan Jeffrey
• [Agda] how does BUILTIN work - practical programming in Agda   Alan Jeffrey
• [Agda] how does BUILTIN work - practical programming in Agda   Alan Jeffrey
• [Agda] Compile-time parsing   Alan Jeffrey
• [Agda] Compiler internals for projection functions   Jeffrey, Alan S A (Alan)
• [Agda] red background when trying to define the Fibonacci sequence   Wolfgang Jeltsch
• [Agda] Auto   Wolfgang Jeltsch
• [Agda] Auto   Wolfgang Jeltsch
• [Agda] LTL Types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs   Wolfgang Jeltsch
• [Agda] Mathematics of Program Construction - first call for papers   Jeremy.Gibbons at comlab.ox.ac.uk
• [Agda] Mathematics of Program Construction: Second Call for Papers   Jeremy.Gibbons at cs.ox.ac.uk
• [Agda] CICM 2012: Call for workshops   Johan Jeuring
• [Agda] First call for papers CICM 2012 - Conference on Intelligent Computer Mathematics   Johan Jeuring
• [Agda] Install failure   Wolfram Kahl
• [Agda] AIM XIII code sprints   Wolfram Kahl
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Wolfram Kahl
• [Agda] RATH-Agda-1.0: Relation-Algebraic Theories in Agda   Wolfram Kahl
• [Agda] Agda without emacs?   Wolfram Kahl
• [Agda] Transitive-on   Wolfram Kahl
• [Agda] Cannot get definitional equality to trigger?   Wolfram Kahl
• [Agda] SOLVED: Cannot get definitional equality to trigger?   Wolfram Kahl
• [Agda] ​Call for Papers: World Congress on Internet Security (WorldCIS-2012)   Paul Kelly
• [Agda] Defining subtraction for naturals   Edward Kmett
• [Agda] interactive mode   Ramana Kumar
• [Agda] subset types? refinement types? type synonyms? type abbreviations?   Ramana Kumar
• [Agda] subset types? refinement types? type synonyms? type abbreviations?   Ramana Kumar
• [Agda] collections/containers/finite sets   Ramana Kumar
• [Agda] subset types? refinement types? type synonyms? type abbreviations?   Ramana Kumar
• [Agda] collections/containers/finite sets   Ramana Kumar
• [Agda] collections/containers/finite sets   Ramana Kumar
• [Agda] collections/containers/finite sets   Ramana Kumar
• [Agda] collections/containers/finite sets   Ramana Kumar
• [Agda] keywords, syntax   Ramana Kumar
• [Agda] interactive evaluation and typechecking   Ramana Kumar
• [Agda] Transitive-on   Ramana Kumar
• [Agda] Transitive-on   Ramana Kumar
• [Agda] strict total order on characters   Ramana Kumar
• [Agda] Re: strict total order on characters   Ramana Kumar
• [Agda] implicit arguments and mixfix   Ramana Kumar
• [Agda] injectivity of Data.Char.toNat?   Ramana Kumar
• [Agda] strict total order on characters   Ramana Kumar
• [Agda] strict total order on characters   Ramana Kumar
• [Agda] strict total order on characters   Ramana Kumar
• [Agda] records and modules   Ramana Kumar
• [Agda] Re: records and modules   Ramana Kumar
• [Agda] links in generated html files   Ramana Kumar
• [Agda] a termination problem   Ramana Kumar
• [Agda] a termination problem   Ramana Kumar
• [Agda] a termination problem   Ramana Kumar
• [Agda] a termination problem   Ramana Kumar
• [Agda] a termination problem   Ramana Kumar
• [Agda] links in generated html files   Ramana Kumar
• [Agda] lhs2tex and agda identifiers   Dan Licata
• [Agda] lhs2tex and agda identifiers   Dan Licata
• [Agda] Termination not being proven   Dan Licata
• [Agda] Universes à la Tarski and induction-recursion   Dan Licata
• [Agda] very basic question about False   Dan Licata
• [Agda] Re: Syntax for anonymous functions [Re: AIM XIII code sprints]   Dan Licata
• [Agda] Agda beginner's problem   Dan Licata
• [Agda] Compile-time parsing   Dan Licata
• [Agda] Are two equal things the same?   Dan Licata
• [Agda] ANN: coq-like agda-mode support for databases of lemmas   Fredrik Lindblad
• [Agda] lhs2tex and agda identifiers   Andres Loeh
• [Agda] Re: Syntax for anonymous functions [Re: AIM XIII code sprints]   Anthony de Almeida Lopes
• [Agda] Recursive types for free?   Anthony de Almeida Lopes
• [Agda] Recursive types for free?   Anthony de Almeida Lopes
• [Agda] Recursive types for free?   Anthony de Almeida Lopes
• [Agda] Agda compiler backend targeting JavaScript   Anthony de Almeida Lopes
• [Agda] curious   Anthony de Almeida Lopes
• [Agda] curious   Anthony de Almeida Lopes
• [Agda] curious   Anthony de Almeida Lopes
• [Agda] curious   Anthony de Almeida Lopes
• [Agda] curious   Anthony de Almeida Lopes
• Study type theory in Europe [Re: [Agda] curious]   Anthony de Almeida Lopes
• Study type theory in Europe [Re: [Agda] curious]   Anthony de Almeida Lopes
• Study type theory in Europe [Re: [Agda] curious]   Anthony de Almeida Lopes
• [Agda] Overlapping patterns in function definition -- strange behavior   Anthony de Almeida Lopes
• [Agda] dependent mutually inductive types   Anthony de Almeida Lopes
• [Agda] Re: Agda running in the browser   Anthony de Almeida Lopes
• [Agda] New release soon   Anthony de Almeida Lopes
• [Agda] Re: 'Dummie' question - why records?   Zhaohui Luo
• [Agda] Documentation of the (not only) latest features   Joe M
• [Agda] type checker   Cecilia Manzino
• [Agda] Agda Observational equality using primUnsafeTrustMe?   Conor McBride
• [Agda] Agda Observational equality using primUnsafeTrustMe?   Conor McBride
• [Agda] Agda Observational equality using primUnsafeTrustMe?   Conor McBride
• [Agda] Agda Observational equality using primUnsafeTrustMe?   Conor McBride
• [Agda] Agda Observational equality using primUnsafeTrustMe?   Conor McBride
• [Agda] Fwd: Course: Introduction to Dependently Typed Programming using Agda   Conor McBride
• [Agda] Fwd: Course: Introduction to Dependently Typed Programming using Agda   Conor McBride
• [Agda] new release   Conor McBride
• [Agda] Extending Pattern Unification to Records   Conor McBride
• Fwd: [Agda] how to count 0..n-1   Conor McBride
• Fwd: [Agda] how to count 0..n-1   Conor McBride
• [Agda] Yet another questions about equality   Conor McBride
• [Agda] termination   Conor McBride
• [Agda] termination   Conor McBride
• [Agda] termination   Conor McBride
• [Agda] Defining subtraction for naturals   Conor McBride
• [Agda] Proving _!_ is inverse of tabulate...   Conor McBride
• [Agda] Another(!) PhD Position at Strathclyde   Conor McBride
• Equality on Types [Re: [Agda] Is this a bug?]   Conor McBride
• [Agda] curious   Conor McBride
• [Agda] PhD Position available at Strathclyde   Conor McBride
• [Agda] Strathclyde PhD Position (new start date)   Conor McBride
• [Agda] Re: Agda running in the browser   Conor McBride
• [Agda] Compile-time parsing   Conor McBride
• [Agda] Compile-time parsing   Conor McBride
• [Agda] Compile-time parsing   Conor McBride
• [Agda] termination   James McKinna
• [Agda] Re: [Haskell-cafe] Defining subtraction for naturals   David Menendez
• [Agda] Re: Syntax for anonymous functions [Re: AIM XIII code sprints]   Stefan Monnier
• [Agda] Re: Agda's unification: postulates versus data types   Stefan Monnier
• [Agda] Proving Parametricity?   Brandon Moore
• [Agda] Proving Parametricity?   Brandon Moore
• [Agda] Proving Parametricity?   Brandon Moore
• [Agda] Dependent injection without K?   Brandon Moore
• [Agda] Automatic generation of trivial proofs   Brandon Moore
• [Agda] refuting with rewrite   Brandon Moore
• [Agda] refuting with rewrite   Brandon Moore
• [Agda] Sharing between records   Brandon Moore
• [Agda] Avoiding implicit argument proliferation?   Brandon Moore
• [Agda] Avoiding implicit argument proliferation?   Brandon Moore
• [Agda] Avoiding implicit argument proliferation?   Brandon Moore
• [Agda] Irrelevance and equalities?   Brandon Moore
• [Agda] Building Coinductive Trees   Brandon Moore
• [Agda] Building Coinductive Trees, Agsy Internal Error   Brandon Moore
• [Agda] Building Coinductive Trees   Brandon Moore
• [Agda] Sized types and coinduction   Brandon Moore
• [Agda] constructor-headed functions to Set   Brandon Moore
• [Agda] Divergence in inference with constructor-headed functions   Brandon Moore
• [Agda] Termination checking with partiality monad   Brandon Moore
• [Agda] Normalization by Evaluation   Brandon Moore
• [Agda] Normalization by Evaluation   Brandon Moore
• [Agda] change in handling of irrelevant parameters (bug?)   Darin Morrison
• [Agda] change in handling of irrelevant parameters (bug?)   Darin Morrison
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Darin Morrison
• [Agda] Lightweight dependency management using make   Darin Morrison
• [Agda] Agda without emacs?   Darin Morrison
• [Agda] WST 2012: First Call For Papers   Georg Moser
• [Agda] WST 2012: Second Call For Papers   Georg Moser
• [Agda] RTA 2012: Second Call For Papers   Georg Moser
• [Agda] Final Call For Papers RTA 2012   Georg Moser
• [Agda] CFP: Foundations of Coordination Languages and Software Architectures (Deadline: June 3)   Mousavi, M.
• [Agda] WGP 2011: Call for Papers   Shin-Cheng Mu
• [Agda] CFP: Certified Programs and Proofs   Shin-Cheng Mu
• [Agda] CFP: APLAS 2011, Kenting, Taiwan   Shin-Cheng Mu
• [Agda] 2nd CFP: ACM SIGPLAN 7th Workshop on Generic Programming (WGP 2011)   Shin-Cheng Mu
• [Agda] LFMTP 2011, Call for Papers   Gopalan Nadathur
• [Agda] LFMTP 2011 Call for Papers (2nd Call)   Gopalan Nadathur
• [Agda] SOS 2011: Call for Papers   Keiko Nakata
• [Agda] SOS 2011: 2nd Call for Papers   Keiko Nakata
• [Agda] FLOPS 2012 call for papers   Keiko Nakata
• [Agda] Install failure   Bengt Nordstrom
• [Agda] Install failure ghc-7.0.2 / cabal solved   Bengt Nordstrom
• [Agda] binder for existential quantifier   Bengt Nordstrom
• [Agda] Agda compiler backend targeting JavaScript   Bengt Nordstrom
• Study type theory in Europe [Re: [Agda] curious]   Bengt Nordstrom
• [Agda] Re: Agda running in the browser   Bengt Nordstrom
• [Agda] Compile-time parsing   Bengt Nordstrom
• [Agda] mutual recursion   Ulf Norell
• [Agda] Problem with a simple proof   Ulf Norell
• [Agda] Impossible proofs about where blocks?   Ulf Norell
• [Agda] Overlapping patterns in function definition -- strange behavior   Ulf Norell
• [Agda] Implicit variables on data constructors   Ulf Norell
• [Agda] Absurd lambdas and equality   Ulf Norell
• [Agda] Implicit variables on data constructors   Ulf Norell
• [Agda] Agda performance improvements   Ulf Norell
• [Agda] Prop was removed in 2.2.8   Ulf Norell
• [Agda] Prop was removed in 2.2.8   Ulf Norell
• [Agda] Re: Problem with propositional equality (or my understanding of it)   Ulf Norell
• [Agda] Inspect on steroids   Ulf Norell
• [Agda] Compiler internals for projection functions   Ulf Norell
• [Agda] Compiler internals for projection functions   Ulf Norell
• [Agda] Mapping QNames to module names?   Ulf Norell
• [Agda] Mapping QNames to module names?   Ulf Norell
• [Agda] Mapping QNames to module names?   Ulf Norell
• [Agda] Agda's coinduction incompatible with initial algebras   Ulf Norell
• [Agda] Mapping QNames to module names?   Ulf Norell
• [Agda] Agda's coinduction incompatible with initial algebras   Ulf Norell
• [Agda] New release soon   Ulf Norell
• [Agda] Agda's coinduction incompatible with initial algebras   Ulf Norell
• [Agda] My coinductive function doesn't termination-check   Ulf Norell
• [Agda] Agda 2.3.0 released   Ulf Norell
• [Agda] Agda 2.3.0 released   Ulf Norell
• [Agda] how does BUILTIN work - practical programming in Agda   Ulf Norell
• [Agda] Record "Setters"?   Liam O'Connor
• [Agda] Record "Setters"?   Liam O'Connor
• [Agda] Associativity for free!   Liam O'Connor
• [Agda] Do-notation with mix fix binders?   Liam O'Connor
• [Agda] Re: Agda Digest, Vol 73, Issue 2   Valeria de Paiva
• [Agda] Defining subtraction for naturals   Luke Palmer
• [Agda] RDP 2011 - Second Call for Participation   Luca Paolini
• [Agda] mutual haskell types with MAlonzo   Perikov Pavel
• [Agda] hello, I've done something terrible...   Perikov Pavel
• Fwd: [Agda] hello, I've done something terrible...   Perikov Pavel
• [Agda] red background when trying to define the Fibonacci sequence   Daniel Peebles
• [Agda] how to count 0..n-1   Daniel Peebles
• [Agda] Applicative with arbitrary morphisms : how ?   Daniel Peebles
• [Agda] Re: comlicated equivalence: need help to prove: errh, addres of repository   Daniel Peebles
• [Agda] Install failure   Daniel Peebles
• [Agda] Process: how to extend the Agda standard library?   Daniel Peebles
• [Agda] Process: how to extend the Agda standard library?   Daniel Peebles
• [Agda] Impossible proofs about where blocks?   Daniel Peebles
• [Agda] Impossible proofs about where blocks?   Daniel Peebles
• [Agda] Overloaded literals   Daniel Peebles
• [Agda] Absurd lambdas and equality   Daniel Peebles
• [Agda] 'Dummie' question - why records?   Daniel Peebles
• [Agda] Associativity for free!   Daniel Peebles
• [Agda] collections/containers/finite sets   Daniel Peebles
• [Agda] how does BUILTIN work - practical programming in Agda   Daniel Peebles
• [Agda] how does BUILTIN work - practical programming in Agda   Daniel Peebles
• [Agda] how does BUILTIN work - practical programming in Agda   Daniel Peebles
• [Agda] Relaxing the strict positivity requirement   Daniel Peebles
• [Agda] Compile-time parsing   Daniel Peebles
• [Agda] repository of Agda code/proofs   Pavel Perikov
• [Agda] Power series in Agda   Pavel Perikov
• [Agda] Passing numerics to haskell   Pavel Perikov
• [Agda] Prop was removed in 2.2.8   Pavel Perikov
• [Agda] Prop was removed in 2.2.8   Pavel Perikov
• [Agda] TLDI 2012 - Call for Papers and Contributed Talks   Benjamin C. Pierce
• [Agda] TLDI 2012 - Call for Papers and Contributed Talks (updated)   Benjamin C. Pierce
• [Agda] TLDI 2012 Call for participation   Benjamin C. Pierce
• [Agda] Associativity for free!   Randy Pollack
• [Agda] Sharing between records   Nicolas Pouillard
• [Agda] Academic reference for the Fin data type   Nicolas Pouillard
• [Agda] Academic reference for the Fin data type   Nicolas Pouillard
• [Agda] Bug in record definition   Nicolas Pouillard
• [Agda] Bug in record definition   Nicolas Pouillard
• [Agda] Irrelevance and equalities?   Nicolas Pouillard
• [Agda] Fixing inferExpr panic   Nicolas Pouillard
• [Agda] AIM XIII code sprints   Nicolas Pouillard
• [Agda] New release soon   Nicolas Pouillard
• [Agda] Mapping QNames to module names?   Nicolas Pouillard
• [Agda] Pattern matching on irrelevant data   Nicolas Pouillard
• [Agda] Pattern matching on irrelevant data   Nicolas Pouillard
• [Agda] Agda's coinduction incompatible with initial algebras   Nicolas Pouillard
• [Agda] Agda's coinduction incompatible with initial algebras   Nicolas Pouillard
• [Agda] Associativity for free!   Nicolas Pouillard
• [Agda] Relaxing the strict positivity requirement   Andrea Lo Pumo
• [Agda] Call for Papers: 3rd Workshop on Modules and Libraries for Proof Assistants (affiliated with ITP 2011)   Florian Rabe
• [Agda] Last Call for Papers: 3rd Workshop on Modules and Libraries for Proof Assistants (affiliated with ITP 2011)   Florian Rabe
• [Agda] Call for Participation: LFMTP/MLPA, August 26, Nijmegen   Florian Rabe
• [Agda] GF Summer School, Barcelona, 15-26 August   Aarne Ranta
• [Agda] Termination Checking   Leonardo Rodriguez
• [Agda] Termination Checking   Leonardo Rodriguez
• [Agda] Termination Checking   Leonardo Rodriguez
• [Agda] CFP: PADL'12 - Practical Aspects of Declarative Languages 2012   Claudio Russo
• [Agda] Second CFP: PADL'12 - Practical Aspects of Declarative Languages 2012   Claudio Russo
• [Agda] Final CFP: PADL'12 - Practical Aspects of Declarative Languages 2012   Claudio Russo
• [Agda] PADL 2012 Call for Participation   Claudio Russo
• [Agda] PADL 2012 Final Call for Participation   Claudio Russo
• [Agda] induction recursion - normalisation   Ondrej Rypacek
• [Agda] Re: induction recursion - normalisation   Ondrej Rypacek
• [Agda] general question   Ondrej Rypacek
• [Agda] mutual recursion   Ondrej Rypacek
• Parameters and indices [Re: [Agda] general question]   Ondrej Rypacek
• Parameters and indices [Re: [Agda] general question]   Ondrej Rypacek
• [Agda] RTA 2012: Call for Workshop Proposals   Masahiko Sakai
• [Agda] Agda without emacs?   Grigory Sarnitskiy
• [Agda] Agda without emacs?   Grigory Sarnitskiy
• [Agda] Are there unicorns in Agda?   Gabriel Scherer
• [Agda] collections/containers/finite sets   Daniel Schoepe
• [Agda] PhD Positions on Trustworthy Electronic Elections   Carsten Schuermann
• [Agda] Two Postdoc Positions at the IT University of Copenhagen   Carsten Schuermann
• [Agda] Logic related PhD studentships available in Swansea, UK   Anton Setzer
• [Agda] PhD studentship related to programming languages   Anton Setzer
• [Agda] hello, I've done something terrible...   Anton Setzer
• [Agda] Extended deadline; IFIP sponsorship: IFIP Working Conference on Domain-Specific Languages   Chung-chieh Shan
• [Agda] LOLA 2011 -- call for contributed talks   Zhong Shao
• [Agda] LOLA 2011 -- Final Call for Contributed Talks (Deadline: April 29th)   Zhong Shao
• [Agda] Post-Doctoral Position at Yale University   Zhong Shao
• [Agda] LOLA 2011 Final Program and Call for Participation   Zhong Shao
• [Agda] hello, I've done something terrible...   Jeremy Shaw
• [Agda] dependent mutually inductive types   Michael Shulman
• [Agda] dependent mutually inductive types   Michael Shulman
• [Agda] very basic question about False   Vincent Siles
• [Agda] very basic question about False   Vincent Siles
• [Agda] A proof of omniscience in Agda   Vincent Siles
• [Agda] Compiler internals for projection functions   Vincent Siles
• [Agda] Coinductive indices   Robert J. Simmons
• [Agda] Coinductive indices   Robert J. Simmons
• [Agda] Compile-time parsing   Ben Sinclair
• [Agda] My coinductive function doesn't termination-check   Nick Smallbone
• [Agda] My coinductive function doesn't termination-check   Nick Smallbone
• [Agda] IICE-2011: Call for Papers!   Margaret Smith
• [Agda] CICE-2012: Call for Papers!   Margaret Smith
• [Agda] Converting a pattern match to an equality   Will Sonnex
• [Agda] Termination not being proven   Will Sonnex
• [Agda] Termination not being proven   Will Sonnex
• [Agda] Termination not being proven   Will Sonnex
• [Agda] Dependent injection without K?   Matthieu Sozeau
• [Agda] PLPV 2012 Call for papers   Matthieu Sozeau
• [Agda] PLPV 2012: Updated Call for Papers   Matthieu Sozeau
• [Agda] Junior researcher position on the FORMATH porject in Nijmegen 6 months.   Bas Spitters
• [Agda] termination   Bas Spitters
• [Agda] Coq Workshop: Call for informal presentations and demonstrations   Bas Spitters
• [Agda] MAP2011   Bas Spitters
• [Agda] Choice sequences and effects   Bas Spitters
• [Agda] 1yr researcher on the formath project   Bas Spitters
• [Agda] Agda beginner's problem   Christian Sternagel
• [Agda] Agda beginner's problem   Christian Sternagel
• [Agda] Agda beginner's problem   Christian Sternagel
• [Agda] Power series in Agda   Wouter Swierstra
• [Agda] ICFP 2011: Second Call for Papers   Wouter Swierstra
• [Agda] ICFP 2011 Deadline Extension   Wouter Swierstra
• [Agda] CFP: DTP'11   Wouter Swierstra
• [Agda] An update on ICFP'11 in Tokyo (September 18-24, 2011)   Wouter Swierstra
• [Agda] DTP 2011: Second Call for Talks   Wouter Swierstra
• [Agda] Call for participation: DTP 2011   Wouter Swierstra
• [Agda] ICFP 2011: Call for participation   Wouter Swierstra
• [Agda] ICFP 2012: Call for workshops and co-located events   Wouter Swierstra
• [Agda] CFP -- Haskell Symposium 2011   Haskell Symposium
• [Agda] 2nd CFP -- Haskell Symposium 2011   Haskell Symposium
• [Agda] Final CFP FLOPS 2012   Peter Thiemann
• [Agda] Compile-time parsing   Peter Thiemann
• [Agda] Compile-time parsing   Peter Thiemann
• [Agda] Compile-time parsing   Peter Thiemann
• [Agda] Compile-time parsing   Peter Thiemann
• [Agda] Invitation to submit a paper to the PSC track @ ACM SAC   Emiliano Tramontana
• [Agda] Call for Paper: PSC track at SAC   Emiliano Tramontana
• [Agda] Problem when getting the Standard Library   Dirk Ullrich
• [Agda] Typechecking failure for Agda Standard Library   Dirk Ullrich
• [Agda] Something like type classes in Agda?   Dirk Ullrich
• [Agda] 'Dummie' question - why records?   Dirk Ullrich
• [Agda] 'Dummie' question - why records?   Dirk Ullrich
• [Agda] 'Dummie' question - why records?   Dirk Ullrich
• [Agda] Building with GHC 7.4   Dirk Ullrich
• [Agda] Building with GHC 7.4   Dirk Ullrich
• [Agda] CfP: 34th IEEE Software Engineering Workshop (SEW-34)   Miroslav Velev
• [Agda] CfP: SARA 2011   Miroslav Velev
• [Agda] Call For Papers: HLDVT 2011   Shireesh Verma
• [Agda] Call for papers: HLDVT 2011 (with a journal special section)   Shireesh Verma
• [Agda] HLDVT 2011: Paper submission deadline extended   Shireesh Verma
• [Agda] HLDVT 2011: 2 days to abstract submission deadline   Shireesh Verma
• [Agda] Install failure ghc-7.0.2 / cabal solved   Andrea Vezzosi
• [Agda] Bug in record definition   Andrea Vezzosi
• [Agda] Agda beginner's problem   Andrea Vezzosi
• [Agda] heap mistery   Andrea Vezzosi
• [Agda] Nice programming challenge   Andrea Vezzosi
• [Agda] Nice programming challenge   Andrea Vezzosi
• [Agda] Irrelevance and propositional equality   Andrea Vezzosi
• [Agda] Irrelevance and propositional equality   Andrea Vezzosi
• [Agda] Re: Associativity for free!   Andrea Vezzosi
• [Agda] Re: Associativity for free!   Andrea Vezzosi
• [Agda] Re: Associativity for free!   Andrea Vezzosi
• [Agda] Lightweight free theorems   Andrea Vezzosi
• [Agda] Size of propositional equality?   Vladimir Voevodsky
• [Agda] Size of propositional equality?   Vladimir Voevodsky
• [Agda] Univalent Foundations program 2012-2013   Vladimir Voevodsky
• [Agda] an update to Foundations   Vladimir Voevodsky
• [Agda] CRA-W/CDC Programming Languages Mentoring Workshop   Stephanie Weirich
• [Agda] REMINDER: Ireland International Conference on Education (IICE-2012): Call for Papers!   L inda Woods
• [Agda] REMINDER: Ireland International Conference on Education (IICE-2012): Call for Papers!   L inda Woods
• [Agda] agda syb 0.3 haskell platform 2011.2.0.1   Mark Wright
• [Agda] agda syb 0.3 haskell platform 2011.2.0.1   Mark Wright
• [Agda] Announcement: Agda Intensive Meeting (AIM) XIV   KINOSHITA Yoshiki
• [yoshiki] Re: [Agda] Associativity for free!   KINOSHITA Yoshiki
• [yoshiki] Re: [Agda] Associativity for free!   KINOSHITA Yoshiki
• [Agda] curious   Guillaume Yziquel
• Study type theory in Europe [Re: [Agda] curious]   Guillaume Yziquel
• [Agda] Hello World   Guillaume Yziquel
• [Agda] Hello World   Guillaume Yziquel
• [Agda] Hello World   Guillaume Yziquel
• [Agda] Re: Syntax for anonymous functions [Re: AIM XIII code sprints]   Noam Zeilberger
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Noam Zeilberger
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Noam Zeilberger
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Noam Zeilberger
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   Noam Zeilberger
• [Agda] research post   Zhaohui.Luo at rhul.ac.uk
• [Agda] Re: Problem when getting the Standard Library   awson
• [Agda] New conference - Certified Programs and Proofs   bywang at iis.sinica.edu.tw
• [Agda] CPP 2011 - Call for Papers   bywang at iis.sinica.edu.tw
• [Agda] Call for Papers: APLAS+CPP (new deadlines)   bywang at iis.sinica.edu.tw
• [Agda] Re: Call for Papers: APLAS+CPP (new deadlines)   bywang at iis.sinica.edu.tw
• [Agda] RTA 2011: extended deadline   Masahiko Sakai (RTA publicity chair)
• [Agda] RDP 2011: Call for Participation   Masahiko Sakai (RTA publicity chair)
• [Agda] Call for Papers: The 6th International Conference for Internet Technology and Secured Transactions (ICITST-2011)!   d.lin at icitst.org
• [Agda] Proving _!_ is inverse of tabulate...   gallais at ensl.org
• [Agda] Proving _!_ is inverse of tabulate...   gallais at ensl.org
• [Agda] Proving _!_ is inverse of tabulate...   gallais at ensl.org
• [Agda] Parsing Mixfix Operators, source code?   gallais at ensl.org
• [Agda] Problem with a simple proof   gallais at ensl.org
• Study type theory in Europe [Re: [Agda] curious]   gallais at ensl.org
• [Agda] Compile-time parsing   gallais at ensl.org
• [Agda] Call for Papers: The 6th International Conference for Internet Technology and Secured Transactions (ICITST-2011)!   g.akmayeva at icitst.org
• [Agda] Converting a pattern match to an equality   gallais
• [Agda] Tricks to limit the memory consumption?   kahl at cas.mcmaster.ca
• [Agda] AIM XIII code sprints   karim kanso
• [Agda] AIM XIII code sprints   karim kanso
• [Agda] Call for Papers: London International Conference on Education!   m.smith at liceducation.org
• [Agda] interactive mode   wren ng thornton
• [Agda] termination   wren ng thornton
• [Agda] Defining subtraction for naturals   wren ng thornton
• [Agda] Defining subtraction for naturals   wren ng thornton
• [Agda] Re: [Haskell-cafe] Defining subtraction for naturals   wren ng thornton
• [Agda] Defining subtraction for naturals   wren ng thornton
• [Agda] Defining subtraction for naturals   wren ng thornton
• [Agda] Install failure   wren ng thornton
• [Agda] Re: Syntax for anonymous functions [Re: AIM XIII code sprints]   wren ng thornton
• [Agda] Re: Syntax for anonymous functions [Re: AIM XIII code sprints]   wren ng thornton
• Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]   wren ng thornton
• Fwd: [Agda] Parallel or   wren ng thornton
• Fwd: [Agda] Parallel or   wren ng thornton
• [Agda] research post   zhaohui at cs.rhul.ac.uk

Last message date: Sat Dec 31 12:22:42 CEST 2011
Archived on: Wed Jan 4 09:59:16 CEST 2012

• Messages sorted by: [ thread ] [ subject ] [ date ]
• More info on this list...