2012 Archives by thread

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

Starting: Wed Jan 4 10:08:36 CEST 2012
Ending: Mon Dec 31 18:45:46 CEST 2012
Messages: 1204

• [Agda] LICS 2012 - Final Call for Papers   Kreutzer, Stephan
• [Agda] WSLST 2012: final announcement   GRLMC
• [Agda] Deadline Extension RTA 2012   Georg Moser
• [Agda] Abstract blocks   karim kanso
  • [Agda] Abstract blocks   Nils Anders Danielsson
• [Agda] induction-recursion   wren ng thornton
  • [Agda] induction-recursion   Anthony de Almeida Lopes
    • [Agda] induction-recursion   wren ng thornton
    • [Agda] induction-recursion   Nils Anders Danielsson
  • [Agda] induction-recursion   Nils Anders Danielsson
• [Agda] CICM 2012: Second call for papers   Johan Jeuring
• [Agda] Installation problem (Windows 7)   Neil P Strickland
  • [Agda] Installation problem (Windows 7)   Nils Anders Danielsson
• [Agda] Turing Centenary Conference in Cambridge - Submission Deadline Jan. 20, 2012   S B Cooper
• [Agda] ​World Congress on Internet Security (WorldCIS-2012): Call for Papers!   Paul Kelly
• [Agda] World Congress on Internet Security (WorldCIS-2012): Call for Papers!   Paul Kelly
• [Agda] red black trees with delete   jleivent at comcast.net
  • [Agda] red black trees with delete   Adam Gundry
  • [Agda] red black trees with delete   Nils Anders Danielsson
    • [Agda] red black trees with delete   Andreas Abel
• [Agda] Irrelevance + instance arguments = inconsistency in 2.3.0   Adam Gundry
  • [Agda] Irrelevance + instance arguments = inconsistency in 2.3.0   Nils Anders Danielsson
  • [Agda] Irrelevance + instance arguments = inconsistency in 2.3.0   Andreas Abel
    • [Agda] Irrelevance + instance arguments = inconsistency in 2.3.0   Andreas Abel
• [Agda] Path to the standard library for the command line compiler   José Pedro Magalhães
  • [Agda] Path to the standard library for the command line compiler   Nils Anders Danielsson
    • [Agda] Path to the standard library for the command line compiler   José Pedro Magalhães
• [Agda] automatically instantiating rewrites   Ramana Kumar
  • [Agda] automatically instantiating rewrites   Nils Anders Danielsson
    • [Agda] automatically instantiating rewrites   Ramana Kumar
      • [Agda] automatically instantiating rewrites   Nils Anders Danielsson
      • [Agda] automatically instantiating rewrites   Ramana Kumar
• [Agda] automatically instantiating rewrites   Ramana Kumar
• [Agda] SSFLA 2012: 2nd announcement   GRLMC
• [Agda] WST 2012: Last Call for Papers and Deadline Extension   Georg Moser
• [Agda] ICFP 2012 Call for papers   Wouter Swierstra
• [Agda] Erasable vs. irrelevant   jleivent at comcast.net
  • [Agda] Erasable vs. irrelevant   Andreas Abel
    • [Agda] Erasable vs. irrelevant   jleivent at comcast.net
      • [Agda] Erasable vs. irrelevant   Andreas Abel
      • [Agda] Erasable vs. irrelevant   jleivent at comcast.net
      • [Agda] Erasable vs. irrelevant   Adam Gundry
      • [Agda] Erasable vs. irrelevant   jleivent at comcast.net
      • [Agda] Erasable vs. irrelevant, and red black trees again   jleivent at comcast.net
      • [Agda] Erasable vs. irrelevant, and red black trees again   Andreas Abel
      • [Agda] Erasable vs. irrelevant, and red black trees again   Conor McBride
      • [Agda] Erasable vs. irrelevant, and red black trees again   Conor McBride
      • [Agda] Erasable vs. irrelevant, and red black trees again   Andreas Abel
      • [Agda] Erasable vs. irrelevant, and red black trees again   Conor McBride
      • [Agda] Erasable vs. irrelevant, and red black trees again   jleivent at comcast.net
      • [Agda] Erasable vs. irrelevant, and red black trees again   Adam Gundry
      • [Agda] Erasable vs. irrelevant, and red black trees again   Alan Jeffrey
      • [Agda] Erasable vs. irrelevant   Dan Doel
    • [Agda] Re: Erasable vs. irrelevant   Stefan Monnier
      • [Agda] Re: Erasable vs. irrelevant   Andreas Abel
• [Agda] Midlands Graduate School 2012   Altenkirch Thorsten
• [Agda] ITP 2012: Final Call for Papers   Amy Felty
• [Agda] Midlands Graduate School 2012   Altenkirch Thorsten
• [Agda] Turing Centenary Conference (CiE 2012) - Final submission arrangements   S B Cooper
• [Agda] [PVS] IIP 2012: Call for Papers   liang chang
• [Agda] MFPS 28 Second Call for Papers   Ulrich Berger
• [Agda] ITP 2013: Call for bids   Lennart Beringer
• [Agda] ICALP 2012 - 2nd Call for Papers   Andrew Pitts
• [Agda] Fun in the Afternoon   Josh Ko
• [Agda] 2nd announcement: workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012)   Hugo Herbelin
• [Agda] MSFP 2012 call for participation   James Chapman
• [Agda] parametrised data structures   James Cranch
  • [Agda] parametrised data structures   Nils Anders Danielsson
    • Positivity annotations [Re: [Agda] parametrised data structures]   Andreas Abel
      • Positivity annotations [Re: [Agda] parametrised data structures]   Dan Doel
• [Agda] Call for Participation: School on Formalization of Mathematics (March 12-16)   Ana Bove
• [Agda] Workshop on Intersection Types and Related Systems (ITRS 2012)   Luca Paolini
• [Agda] Call for Papers - Haskell Symposium 2012   Janis Voigtländer
• [Agda] Call for Participation: Midlands Graduate School 2012   Eike Ritter
• [Agda] Asynchronous Emacs mode / Interactive syntax highlighting   Guilhem Moulin
  • [Agda] Asynchronous Emacs mode / Interactive syntax highlighting   Nils Anders Danielsson
  • [Agda] Asynchronous Emacs mode / Interactive syntax highlighting   Guilhem Moulin
• [Agda] LATA 2012: call for participation   GRLMC
• [Agda] WADT 2012: First Call for Papers   WADT 2012
  • [Agda] WADT 2012: Second Call for Papers   WADT 2012
• [Agda] ​Ireland International Conference on Education (IICE-2012): Final Call for Papers!   John Williams
• [Agda] World Congress on Internet Security (WorldCIS-2012): Call for Papers!   Paul Kelly
• [Agda] WSMBio 2012: final announcement   GRLMC
• [Agda] Coloring of mixfix identifiers   Andreas Abel
  • [Agda] Coloring of mixfix identifiers   Jean-Philippe Bernardy
    • [Agda] Coloring of mixfix identifiers   Andreas Abel
    • [Agda] Re: Coloring of mixfix identifiers   Stefan Monnier
      • [Agda] Re: Coloring of mixfix identifiers   Nils Anders Danielsson
  • [Agda] Re: Coloring of mixfix identifiers   Nils Anders Danielsson
    • [Agda] Re: Coloring of mixfix identifiers   Andreas Abel
• [Agda] Are there unicorns in Agda?   Martin Escardo
  • [Agda] Are there unicorns in Agda?   Vladimir Voevodsky
    • [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?   Jacques Carette
• [Agda] Call for Papers: International Conference on Information Society (i-Society 2012)!   Mark Newman
• [Agda] Strange way of displaying \sqcap and \sqcup in emacs 23.3.1 Lubuntu 11.10   David Wahlstedt
  • [Agda] Strange way of displaying \sqcap and \sqcup in emacs 23.3.1 Lubuntu 11.10   Daniel Schoepe
    • [Agda] Strange way of displaying \sqcap and \sqcup in emacs 23.3.1 Lubuntu 11.10   David Wahlstedt
      • [Agda] Strange way of displaying \sqcap and \sqcup in emacs 23.3.1 Lubuntu 11.10   Daniel Schoepe
• [Agda] Are there unicorns in Agda?   Peter Hancock
  • [Agda] Are there unicorns in Agda?   Martin Escardo
    • [Agda] Are there unicorns in Agda?   Martin Escardo
• [Agda] Strange way of displaying \sqcap and \sqcup in emacs 23.3.1 Lubuntu 11.10   David Wahlstedt
  • [Agda] Strange way of displaying \sqcap and \sqcup in emacs 23.3.1 Lubuntu 11.10   Nils Anders Danielsson
    • [Agda] Strange way of displaying \sqcap and \sqcup in emacs 23.3.1 Lubuntu 11.10   David Wahlstedt
• [Agda] SSNC 2012: 1st announcement   GRLMC
• [Agda] Any examples of monad use in Agda?   jleivent at comcast.net
  • [Agda] Any examples of monad use in Agda?   Andreas Abel
    • [Agda] Any examples of monad use in Agda?   jleivent at comcast.net
      • [Agda] Any examples of monad use in Agda?   Andreas Abel
      • Erasable Monad (was Re: [Agda] Any examples of monad use in Agda?)   jleivent at comcast.net
      • Erasable Monad (was Re: [Agda] Any examples of monad use in Agda?)   Andreas Abel
      • Erasable Monad (was Re: [Agda] Any examples of monad use in Agda?)   jleivent at comcast.net
  • [Agda] Any examples of monad use in Agda?   Alan Jeffrey
• [Agda] Last CFP FORMAL METHODS 2012   Hanna Klaudel
• [Agda] Conference on Intelligent Computer Mathematics, last call for papers   Johan Jeuring
  • [Agda] Conference on Intelligent Computer Mathematics, call for work-in-progress papers   Johan Jeuring
• [Agda] Termination checking on coinduction   Alex Rozenshteyn
  • [Agda] Termination checking on coinduction   Nils Anders Danielsson
    • [Agda] Termination checking on coinduction   Alex Rozenshteyn
      • [Agda] Termination checking on coinduction   Alex Rozenshteyn
      • [Agda] Termination checking on coinduction   Nils Anders Danielsson
      • [Agda] Termination checking on coinduction   Alex Rozenshteyn
      • [Agda] Termination checking on coinduction   Nils Anders Danielsson
• [Agda] SSFLA 2012: 3rd announcement   GRLMC
• [Agda] POPL'13: Call for proposals for co-located events   Viktor Vafeiadis
• [Agda] ITP 2013: final call for bids   Lennart Beringer
• [Agda] MFPS 28 Final Call for Papers   Ulrich Berger
• [Agda] Pattern matching order?   Brandon Moore
  • [Agda] Call for papers: special issue of MSCS   Thierry Coquand
  • [Agda] Pattern matching order?   Nils Anders Danielsson
• [Agda] complex indices   Ramana Kumar
  • [Agda] complex indices   Brandon Moore
    • [Agda] complex indices   Ramana Kumar
  • [Agda] complex indices   Andreas Abel
    • [Agda] complex indices   Ramana Kumar
      • [Agda] complex indices   Andreas Abel
      • [Agda] complex indices   Ramana Kumar
• [Agda] complex indices   Ramana Kumar
  • [Agda] complex indices   Brandon Moore
• [Agda] [CiE 2012] Call for Informal Presentations for Turing Centenary Conference in Cambridge   S B Cooper
• [Agda] MFPS 28: paper submission deadline extended by one week   U.Berger at swansea.ac.uk
• [Agda] Working with coinductive trees?   Brandon Moore
  • [Agda] Working with coinductive trees?   Nils Anders Danielsson
    • [Agda] Working with coinductive trees?   Brandon Moore
• [Agda] ETAPS Workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012)   Hugo Herbelin
• [Agda] TPNC 2012: 1st call for papers   GRLMC
• [Agda] private fields in records?   jleivent at comcast.net
  • [Agda] private fields in records?   Andreas Abel
• [Agda] Conversion bug   James Cranch
  • [Agda] Conversion bug   Nils Anders Danielsson
• [Agda] Alan Turing Centenary Conference, University of Manchester, 22-25 June, 2012   S B Cooper
• [Agda] CALL FOR PAPERS   Al-mukhatabat Journal
• [Agda] CFP: Workshop on Generic Programming 2012   Andres Loeh
• [Agda] 2nd Call for Participation: Midlands Graduate School 2012   E.Ritter at cs.bham.ac.uk
• [Agda] How to disable type-checking progress in emacs buffer?   Peter Hancock
  • [Agda] How to disable type-checking progress in emacs buffer?   Guilhem Moulin
    • [Agda] How to disable type-checking progress in emacs buffer?   Guilhem Moulin
  • [Agda] How to disable type-checking progress in emacs buffer?   Nils Anders Danielsson
• [Agda] World's biggest fake conference in computer science   James Allen
• [Agda] Turing Centenary Meeting, Chinese Academy of Sciences, Beijing, China   S B Cooper
• [Agda] SSNC 2012: 2nd announcement   GRLMC
• [Agda] Declaration-wise termination checking.   Andreas Abel
• [Agda] Intersection Types and Related Systems (ITRS 2012) -- 2nd CFP   Luca Paolini
• [Agda] Fwd: categories: PhD position available   Conor McBride
• [Agda] SSFLA 2012: final announcement   GRLMC
• [Agda] Agda 2.3.0.1   Ulf Norell
• [Agda] HOR 2012: Call for papers   Andreas Abel
• [Agda] A demonstration of Agda   Alan Jeffrey
  • [Agda] A demonstration of Agda   Anthony de Almeida Lopes
• [Agda] Chairman disappears from world's biggest computer conference   James Allen
• [Agda] Open DemTech PhD positions @ ITU   Carsten Schürmann
• [Agda] Re: Associativity for free!   Andreas Abel
  • [Agda] Re: Associativity for free!   Alan Jeffrey
    • [Agda] Re: Associativity for free!   Andreas Abel
      • [Agda] Re: Associativity for free!   Alan Jeffrey
• [Agda] Recursive Sets / refine vs. load   Brandon Moore
  • [Agda] Recursive Sets / refine vs. load   Peter Hancock
  • [Agda] Recursive Sets / refine vs. load   Nils Anders Danielsson
    • [Agda] Recursive Sets / refine vs. load   Altenkirch Thorsten
      • [Agda] Recursive Sets / refine vs. load   Andreas Abel
      • [Agda] Recursive Sets / refine vs. load   Altenkirch Thorsten
      • Interleaving typechecking and evaluation [Re: [Agda] Recursive Sets / refine vs. load]   Andreas Abel
      • Interleaving typechecking and evaluation [Re: [Agda] Recursive Sets / refine vs. load]   Wolfram Kahl
      • Interleaving typechecking and evaluation [Re: [Agda] Recursive Sets / refine vs. load]   Andreas Abel
• [Agda] TPNC 2012: 2nd call for papers   GRLMC
• [Agda] Wildcards   Guillaume Brunerie
  • [Agda] Wildcards   Nils Anders Danielsson
    • [Agda] Wildcards   Guillaume Brunerie
      • [Agda] Wildcards   Andreas Abel
• [Agda] Call for Participation: RTA 2012   Georg Moser
• [Agda] Intersection Types and Related Systems (ITRS 2012) -- Final Call   Luca Paolini
• No longer yellow, for your satisfaction [Re: [Agda] some yellow, for your amusement]   Andreas Abel
  • No longer yellow, for your satisfaction [Re: [Agda] some yellow, for your amusement]   Conor McBride
• [Agda] WADT 2012: Final Call for Papers   WADT 2012
• [Agda] CALL FOR PARTICIPATION: FLOPS 2012   Peter Thiemann
• [Agda] CfP: Math Information Retrieval Worksohp 14. July 2012   m.kohlhase at jacobs-university.de
• [Agda] CFP: CPP 2012 - 2nd International Conference on Certified Programs and Proofs   Chris Hawblitzel
• [Agda] parse errors with the latest version   Ondrej Rypacek
  • [Agda] parse errors with the latest version   Dominique Devriese
• [Agda] parse errors with the latest version   Dan Rosén
• [Agda] Build error for Agda from Darcs   Dirk Ullrich
  • [Agda] Build error for Agda from Darcs   Andreas Abel
• [Agda] A frontend for the semiring solver using the reflection API   Wojciech Jedynak
  • [Agda] A frontend for the semiring solver using the reflection API   Andreas Abel
  • [Agda] A frontend for the semiring solver using the reflection API   Altenkirch Thorsten
    • [Agda] A frontend for the semiring solver using the reflection API   Ramana Kumar
• [Agda] WADT 2012: Deadline Extension   WADT 2012
• [Agda] A frontend for the semiring solver using the reflection API   Wojciech Jedynak
• [Agda] Call for papers (deadline change): LFMTP'12 (colocated with ICFP'12)   Adam Chlipala
• [Agda] Call for papers: Types for Proofs and Programs   Bengt Nordstrom
• [Agda] Unreadable constraints, problem with name printing?   Andreas Abel
• [Agda] Call for Papera - Automated Theory Exploration (ATx)   Peter Höfner
• [Agda] TPNC 2012: 3rd call for papers   GRLMC
• [Agda] Alan Turing Centenary Conference in Manchester, 2nd Call for Papers   S B Cooper
• [Agda] 2nd Call for Participation: RTA 2012   Georg Moser
• [Agda] Where did the Dependently Typed Programming in Agda tutorial move to?   Jason Dagit
  • [Agda] Where did the Dependently Typed Programming in Agda tutorial move to?   Daniel Schoepe
• [Agda] SSLST 2012: 1st announcement   GRLMC
• [Agda] Short proof of falsity   Anton Setzer
  • [Agda] Short proof of falsity   Paul van der Walt
  • [Agda] Short proof of falsity   Ulf Norell
• [Agda] Short proof of falsity   Dan Rosén
• [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes   James Deikun
  • [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes   Alan Jeffrey
    • [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes   Daniel Peebles
      • [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes   Alan Jeffrey
      • [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes   Daniel Peebles
      • [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes   Alan Jeffrey
  • [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes   Nils Anders Danielsson
    • [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes   James Deikun
      • [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes   Andreas Abel
      • [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes   Nils Anders Danielsson
• [Agda] SSNC 2012: 3rd announcement   GRLMC
• [Agda] 2nd Call for Informal Presentations at Turing Centenary Conference, Cambridge, UK   S B Cooper
• [Agda] Parametricity is inconsistent with classical logic   Arseniy Alekseyev
  • [Agda] Parametricity is inconsistent with classical logic   Altenkirch Thorsten
  • [Agda] Parametricity is inconsistent with classical logic   Jean-Philippe Bernardy
  • [Agda] Parametricity is inconsistent with classical logic   Benja Fallenstein
    • [Agda] Parametricity is inconsistent with classical logic   Benja Fallenstein
    • [Agda] Parametricity is inconsistent with classical logic   Danko Ilik
      • [Agda] Parametricity is inconsistent with classical logic   Jean-Philippe Bernardy
      • [Agda] Parametricity is inconsistent with classical logic   Nils Anders Danielsson
      • [Agda] Parametricity is inconsistent with classical logic   Martin Escardo
      • [Agda] Parametricity is inconsistent with classical logic   Danko Ilik
      • [Agda] Parametricity is inconsistent with classical logic   Martin Escardo
      • [Agda] Parametricity is inconsistent with classical logic   Martin Escardo
      • [Agda] Parametricity is inconsistent with classical logic   Danko Ilik
      • [Agda] Parametricity is inconsistent with classical logic   Martin Escardo
      • [Agda] Parametricity is inconsistent with classical logic   Peter Hancock
      • [Agda] Parametricity is inconsistent with classical logic   Altenkirch Thorsten
      • [Agda] Parametricity is inconsistent with classical logic   Peter Hancock
      • [Agda] Parametricity is inconsistent with classical logic   Martin Escardo
      • [Agda] Parametricity is inconsistent with classical logic   Bas Spitters
      • [Agda] Parametricity is inconsistent with classical logic   Martin Escardo
• [Agda] SSMBio 2012: 1st announcement   GRLMC
• [Agda] Call for Papers - Haskell Symposium 2012 - six weeks to go   Janis Voigtländer
• [Agda] [BUG] builtins strike again -- Nat is a ring?   James Deikun
  • Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]   Andreas Abel
    • Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]   Nils Anders Danielsson
    • Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]   Nils Anders Danielsson
      • Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]   Ulf Norell
      • Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]   James Deikun
      • Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]   Nils Anders Danielsson
      • Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]   James Deikun
      • Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]   Nils Anders Danielsson
      • Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]   Andreas Abel
• [Agda] interaction interface   Peter Divianszky
  • [Agda] interaction interface   Ramana Kumar
• [Agda] TPNC 2012: submission deadline extended   GRLMC
• [Agda] SSNC 2012: final announcement   GRLMC
• [Agda] strict unit type   Vladimir Voevodsky
  • [Agda] Re: strict unit type   Guillaume Brunerie
    • [Agda] Re: strict unit type   Vladimir Voevodsky
      • [Agda] Re: strict unit type   Guillaume Brunerie
      • [Agda] Re: strict unit type   Dan Doel
      • [Agda] Re: strict unit type   Andreas Abel
      • [Agda] Re: strict unit type   Vladimir Voevodsky
      • [Agda] Re: strict unit type   Andreas Abel
      • [Agda] Re: strict unit type   Vladimir Voevodsky
      • [Agda] Re: strict unit type   Andreas Abel
      • [Agda] Re: strict unit type   Vladimir Voevodsky
      • [Agda] Re: strict unit type   Andreas Abel
• [Agda] Re: Performance gains for normalization when dumping IO?   James Deikun
• [Agda] Re: [TYPES] strict unit type   Altenkirch Thorsten
  • [Agda] Re: [TYPES] strict unit type   Vladimir Voevodsky
    • [Agda] Re: [TYPES] strict unit type   Altenkirch Thorsten
• [Agda] Postdoc opportunities in functional programming & formal verification   Adam Chlipala
• [Agda] : vs. ∶   Wolfgang Jeltsch
  • Re: [Agda] : vs. ∶   Jean-Philippe Bernardy
  • [Agda] : vs. ∶   Martin Escardo
    • Re: [Agda] : vs. ∶   Andrew Pitts
    • Re: [Agda] : vs. ∶   Dominique Devriese
  • [Agda] : vs. ∶   Nils Anders Danielsson
    • [Agda] : vs. ∶   Wolfram Kahl
      • [Agda] : vs. ∶   Nils Anders Danielsson
      • [Agda] : vs. ∶   Wolfram Kahl
    • [Agda] : vs. ∶   Andreas Abel
      • [Agda] : vs. ∶   Nils Anders Danielsson
      • [Agda] : vs. ∶   Cezar Ionescu
      • [Agda] : vs. ∶   Alan Jeffrey
      • [Agda] : vs. ∶   Wolfgang Jeltsch
      • [Agda] : vs. ∶   Nils Anders Danielsson
      • Re: [Agda] : vs. ∶   Darryl
      • [Agda] : vs. ∶   Wolfgang Jeltsch
      • [Agda] : vs. ∶   Nils Anders Danielsson
      • Re: [Agda] : vs. ：   Altenkirch Thorsten
      • [Agda] goal normalization request   Darryl
      • [Agda] goal normalization request   Andreas Abel
      • [Agda] goal normalization request   Nils Anders Danielsson
      • [Agda] goal normalization request   Darryl
      • Re: [Agda] : vs. ∶   Dominique Devriese
      • [Agda] : vs. ∶   Wolfgang Jeltsch
  • Re: [Agda] : vs. ∶   Jean-Philippe Bernardy
• [Agda] all functions have the same graph   Martin Escardo
• [Agda] Fwd: Fix for `geniplate' to build with `template-haskell-2.7.0.0', too   Dirk Ullrich
  • [Agda] Fwd: Fix for `geniplate' to build with `template-haskell-2.7.0.0', too   Wojciech Jedynak
    • [Agda] Fwd: Fix for `geniplate' to build with `template-haskell-2.7.0.0', too   Nils Anders Danielsson
• [Agda] CiE 2012: Turing Centenary Conference, Cambridge - Final Call for Presentations   S B Cooper
• [Agda] SSLST 2012: 2nd announcement   GRLMC
• [Agda] importing a module from a module   Andreas Abel
  • [Agda] importing a module from a module   Nils Anders Danielsson
• [Agda] CFP: Workshop on Generic Programming 2012 (co-located with ICFP)   Andres Loeh
• [Agda] Bounties for Agda features   Daniel Peebles
  • [Agda] Bounties for Agda features   Andreas Abel
    • [Agda] Bounties for Agda features   Daniel Peebles
      • [Agda] Bounties for Agda features   Peter Hancock
      • [Agda] Re: Bounties for Agda features   Thomas Hallgren
      • Unfolding and Rewriting [Re: [Agda] Bounties for Agda features]   Andreas Abel
    • [Agda] Bounties for Agda features   Nils Anders Danielsson
• [Agda] [ANN] Agda Intensive Meeting 16th (AIM XVI) in Copenhagen   Nicolas Pouillard
• [Agda] TPNC 2012: last submission deadline extension   URV - RESEARCH GROUP ON MATHEMATICAL LINGUISTICS
• [Agda] practical integer/rational arithmetic?   Noam Zeilberger
  • [Agda] practical integer/rational arithmetic?   Daniel Peebles
    • [Agda] practical integer/rational arithmetic?   Noam Zeilberger
  • [Agda] practical integer/rational arithmetic?   Jacques Carette
    • [Agda] practical integer/rational arithmetic?   Daniel Peebles
      • [Agda] practical integer/rational arithmetic?   James Deikun
    • [Agda] practical integer/rational arithmetic?   Nils Anders Danielsson
      • [Agda] practical integer/rational arithmetic?   Jacques Carette
      • [Agda] practical integer/rational arithmetic?   wren ng thornton
• [Agda] Strict positivity and indices   Dan Doel
  • [Agda] Strict positivity and indices   Nils Anders Danielsson
    • [Agda] Re: Strict positivity and indices   Stefan Monnier
      • [Agda] Re: Strict positivity and indices   Nils Anders Danielsson
      • [Agda] Re: Strict positivity and indices   Andreas Abel
      • [Agda] Re: Strict positivity and indices   Nils Anders Danielsson
      • [Agda] Re: Strict positivity and indices   Andreas Abel
      • [Agda] Re: Strict positivity and indices   Ulf Norell
• [Agda] Call for papers GandALF 2012 -- EXTENDED DEADLINE   Nello Murano
• [Agda] Re: [TYPES] strict unit type   Altenkirch Thorsten
• [Agda] Re: [TYPES] strict unit type   Altenkirch Thorsten
  • [Agda] Re: [TYPES] strict unit type   Robert Harper
    • [Agda] Re: [TYPES] strict unit type   Vladimir Voevodsky
      • [Agda] Re: [TYPES] strict unit type   Robert Harper
      • [Agda] Re: [TYPES] strict unit type   Robert Harper
      • [Agda] Re: [TYPES] strict unit type   Andreas Abel
• [Agda] problem using "with"   Guillermo Calderón
  • [Agda] problem using "with"   Ulf Norell
    • [Agda] Re: problem using "with"   Guillermo Calderón
      • [Agda] Re: problem using "with"   Ulf Norell
      • [Agda] Re: problem using "with"   Wolfram Kahl
      • [Agda] Re: problem using "with"   Nils Anders Danielsson
      • [Agda] Re: problem using "with"   Guillermo Calderón
      • [Agda] Re: problem using "with"   Nils Anders Danielsson
      • [Agda] Re: problem using "with"   Altenkirch Thorsten
      • [Agda] Re: problem using "with"   Nils Anders Danielsson
      • [Agda] Re: problem using "with"   Altenkirch Thorsten
      • [Agda] Re: problem using "with"   Nils Anders Danielsson
      • [Agda] Re: problem using "with"   Altenkirch Thorsten
      • [Agda] Re: problem using "with"   Guillermo Calderón
      • [Agda] Re: problem using "with"   Nils Anders Danielsson
• [Agda] SSMBio 2012: 2nd announcement   GRLMC
• [Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect   Andreas Abel
  • [Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect   Altenkirch Thorsten
    • [Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect   Gabriel Scherer
  • [Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect   Benja Fallenstein
    • [Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect   Andreas Abel
  • [Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect   Nils Anders Danielsson
    • [Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect   Ulf Norell
      • [Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect   Daniel Peebles
      • [Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect   Andreas Abel
      • [Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect   Nils Anders Danielsson
  • [Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect   Dan Doel
• [Agda] Weird constraint on type of a record field   Dr. ERDI Gergo
  • [Agda] Weird constraint on type of a record field   Andreas Abel
• [Agda] MFPS 28: Programme and Call for Participation   Ulrich Berger
• [Agda] Re: [Coq-Club] Positivity condition and nested recursion   Andreas Abel
• [Agda] Workshop "Réalisabilité in Chambéry #5"   Pierre Hyvernat
• [Agda] Postulated computing quotients are unsound   Nils Anders Danielsson
  • [Agda] Postulated computing quotients are unsound   Altenkirch Thorsten
    • [Agda] Postulated computing quotients are unsound   Nils Anders Danielsson
      • [Agda] Postulated computing quotients are unsound   Conor McBride
  • [Agda] Postulated computing quotients are unsound   Dan Licata
  • [Agda] Postulated computing quotients are unsound   Dominique Devriese
    • [Agda] Postulated computing quotients are unsound   Benja Fallenstein
  • [Agda] Postulated computing quotients are unsound   Benja Fallenstein
    • [Agda] Postulated computing quotients are unsound   Dan Licata
      • [Agda] Postulated computing quotients are unsound   Dan Doel
      • [Agda] Postulated computing quotients are unsound   Dan Licata
• [Agda] Re: Poll: Mixfix and parametrized modules --- which behavior would you expect   Darin Morrison
• [Agda] 2nd CFP: CPP 2012 - 2nd International Conference on Certified Programs and Proofs   Chris Hawblitzel
• [Agda] Your favourite date for AIM XVII (Spring 2013)?   KINOSHITA Yoshiki
  • [Agda] Your favourite date for AIM XVII (Spring 2013)?   Bengt Nordstrom
    • [yk] Re: [Agda] Your favourite date for AIM XVII (Spring 2013)?   KINOSHITA Yoshiki
  • [Agda] Re: Your favourite date for AIM XVII (Spring 2013)?   KINOSHITA Yoshiki
• [Agda] FSFLA 2012: 1st announcement   GRLMC
• [Agda] CICM 2012: Call for participation   Johan Jeuring
  • [Agda] CICM 2012: 2nd Call for participation; early registration deadline approaching   Johan Jeuring
    • [Agda] CICM 2012: Programme details on-line, last call for participation   Johan Jeuring
• [Agda] Call for Papers: Implementation and Application of Functional Languages 2012   Tom Harper
• [Agda] MPC2012 Call for Participation   Jeremy.Gibbons at cs.ox.ac.uk
• [Agda] ITP 2012: preliminary call for participation   Lennart Beringer
• [Agda] Final CFP: Workshop on Generic Programming (WGP) 2012   Andres Loeh
• [Agda] IEEE HLDVT 2012: Call for Papers   Hiren Patel
• [Agda] CiE 2012 Turing Centenary Conference, Cambridge - Final Call for Participation   S B Cooper
• [Agda] GAMES 2012 -- Call for contributions --   Nello Murano
• [Agda] SSLST 2012: 3rd announcement   GRLMC
• [Agda] Turing Centenary Conference, Manchester, June 22-25: Call for Participation   S B Cooper
• [Agda] New: Syntax for let pattern bindings   Andreas Abel
  • [Agda] New: Syntax for let pattern bindings   Nicolas Pouillard
  • [Agda] New: Syntax for let pattern bindings   Wolfram Kahl
    • [Agda] New: Syntax for let pattern bindings   Andreas Abel
• [Agda] SSMBio 2012: 3rd announcement   GRLMC
• [Agda] Absurd pattern; convincing Agda   Paul van der Walt
  • [Agda] Absurd pattern; convincing Agda   Andreas Abel
    • [Agda] Absurd pattern; convincing Agda   Daniel Peebles
      • [Agda] Absurd pattern; convincing Agda   Andreas Abel
• [Agda] Influencing pattern matching order [Was: Absurd pattern; convincing Agda]   Dominique Devriese
  • [Agda] Influencing pattern matching order [Was: Absurd pattern; convincing Agda]   Nils Anders Danielsson
• [Agda] Lectureship within the MSP group, Strathclyde   Robert Atkey
• [Agda] CFP: MIR 2012--Mathematics Information Retrieval, Bremen, July 8th   mir2012 at easychair.org
• [Agda] Senior lecturer in Logic of Programs in University of Gothenburg, Sweden   Bengt Nordstrom
• [Agda] Problem with reversing vector   Lyndon Maydwell
  • [Agda] Problem with reversing vector   Dominique Devriese
    • [Agda] Problem with reversing vector   Lyndon Maydwell
• [Agda] PEPM 2012: Call for Papers   Shin-Cheng Mu
• [Agda] Typechecking a module using Haskell   TOmmo Ceee
  • [Agda] Typechecking a module using Haskell   Lyndon Maydwell
• [Agda] expanding solved wildcards   Ramana Kumar
  • [Agda] expanding solved wildcards   Nils Anders Danielsson
• [Agda] LICS 2012 - Last Call for Participation   Andrzej Murawski
• [Agda] without-K problem   Altenkirch Thorsten
  • [Agda] without-K problem   Guillaume Brunerie
    • [Agda] without-K problem   Andreas Abel
• [Agda] ITP2012: call for participation   Lennart Beringer
• [Agda] without-K problem   Altenkirch Thorsten
  • [Agda] without-K problem   Andreas Abel
    • [Agda] without-K problem   Nils Anders Danielsson
      • [Agda] without-K problem   Andreas Abel
      • [Agda] without-K problem   Nils Anders Danielsson
• [Agda] More powerful quoting & reflection?   Paul van der Walt
  • [Agda] More powerful quoting & reflection?   James Deikun
    • [Agda] More powerful quoting & reflection?   Altenkirch Thorsten
• [Agda] Agda memory leaks?   Wolfram Kahl
• [Agda] Termination checker: indirect subterms used in "where" clauses   Guillaume Brunerie
  • [Agda] Termination checker: indirect subterms used in "where" clauses   gallais at ensl.org
    • [Agda] Termination checker: indirect subterms used in "where" clauses   Guillaume Brunerie
• [Agda] IEEE HLDVT 2012: Call for Papers (Submission Deadline Extended: June 29, 2012)   Hiren D. Patel
• [Agda] SSLST 2012: final announcement   GRLMC
• [Agda] ICFP Student Research Competition   Wouter Swierstra
• [Agda] Bug in ScopeMonad?   Paul van der Walt
  • [Agda] Bug in ScopeMonad?   Nils Anders Danielsson
  • [Agda] Bug in ScopeMonad?   Andreas Abel
    • [Agda] Bug in ScopeMonad?   Paul van der Walt
• [Agda] FSFLA 2012: 2nd announcement   GRLMC
• [Agda] ICFP 2012: Call for participation   Wouter Swierstra
• [Agda] Patch for QuickFix 2.5   Dirk Ullrich
• [Agda] Several open Postdoc Positions at the IT University of Copenhagen/DemTech   Carsten Schürmann
  • [Agda] Several open Postdoc Positions at the IT University of Copenhagen/DemTech   Carsten Schürmann
• [Agda] VMCAI 2013: Call for Papers   Josh Berdine
• [Agda] Instance arguments for parametrized modules   Guillaume Brunerie
  • [Agda] Instance arguments for parametrized modules   Andreas Abel
    • [Agda] Instance arguments for parametrized modules   Guillaume Brunerie
      • [Agda] Instance arguments for parametrized modules   Andreas Abel
      • [Agda] Instance arguments for parametrized modules   Andreas Abel
• [Agda] agda halting problem   Ondrej Rypacek
  • [Agda] agda halting problem   Daniel Peebles
    • [Agda] agda halting problem   Dan Doel
      • [Agda] agda halting problem   Andreas Abel
      • [Agda] agda halting problem   Nils Anders Danielsson
  • [Agda] agda halting problem   Andreas Abel
    • [Agda] agda halting problem   Wolfram Kahl
      • [Agda] agda halting problem   Nils Anders Danielsson
• [Agda] Several open Postdoc Positions at the IT University of Copenhagen/DemTech   Carsten Schürmann
• [Agda] SSMBio 2012: final announcement   GRLMC
• [Agda] TPNC 2012: call for posters   GRLMC
• [Agda] SSLST 2012: call for participation   GRLMC
• [Agda] CALL FOR PARTICIPATION - Relational and Algebraic Methods in Computer Science (RAMiCS)   Peter Höfner
• [Agda] Agda for CA   Serge D. Mechveliani
  • [Agda] Agda for CA   Andreas Abel
    • [Agda] Agda for CA   Nils Anders Danielsson
• [Agda] irrelevant fields and EqReasoning   Noam Zeilberger
  • [Agda] irrelevant fields and EqReasoning   Andreas Abel
    • [Agda] irrelevant fields and EqReasoning   Noam Zeilberger
      • [Agda] irrelevant fields and EqReasoning   Andreas Abel
      • [Agda] irrelevant fields and EqReasoning   Noam Zeilberger
      • [Agda] irrelevant fields and EqReasoning   Jean-Philippe Bernardy
      • [Agda] irrelevant fields and EqReasoning   Noam Zeilberger
      • [Agda] irrelevant fields and EqReasoning   Jean-Philippe Bernardy
      • [Agda] irrelevant fields and EqReasoning   Nils Anders Danielsson
      • [Agda] irrelevant fields and EqReasoning   Noam Zeilberger
      • [Agda] irrelevant fields and EqReasoning   Nils Anders Danielsson
• [Agda] Final Call For Papers: Implementation and Application of Functional Languages 2012, Oxford, UK   Tom Harper
• [Agda] CFP: Programming for Separation of Concerns at ACM SAC 2013   Emiliano Tramontana
• [Agda] IEEE HLDVT 2012: Call for Work-in-Progress Abstracts   Hiren D. Patel
• [Agda] PEPM 2013: Second Call for Papers   Shin-Cheng Mu
• [Agda] Norell's tutorial   Serge D. Mechveliani
• [Agda] Agda IO - accessing command-line arguments   stvienna wiener
  • [Agda] Agda IO - accessing command-line arguments   Andreas Abel
• [Agda] compiling Hello.agda   Serge D. Mechveliani
  • [Agda] compiling Hello.agda   James Deikun
  • [Agda] compiling Hello.agda   Paul van der Walt
    • [Agda] compiling Hello.agda   Serge D. Mechveliani
      • [Agda] compiling Hello.agda   Andreas Abel
• [Agda] Call for Papers: Ireland International Conference on Education (IICE-2012)   L inda Woods
• [Agda] beginner questions   Serge D. Mechveliani
  • [Agda] beginner questions   Andreas Abel
  • [Agda] beginner questions   Nils Anders Danielsson
• [Agda] printing to String   Serge D. Mechveliani
  • [Agda] printing to String   Andreas Abel
• [Agda] making Agda on Lenny Debian   Serge D. Mechveliani
  • [Agda] making Agda on Lenny Debian   Wolfram Kahl
• [Agda] making Agda on Lenny Debian   Dan Rosén
• [Agda] PLPV 2013 First Call for Papers   Andreas Abel
• [Agda] Display of private things (for higher inductive types)   Guillaume Brunerie
  • [Agda] Display of private things (for higher inductive types)   Andreas Abel
    • [Agda] Display of private things (for higher inductive types)   Guillaume Brunerie
      • [Agda] Display of private things (for higher inductive types)   Nils Anders Danielsson
• [Agda] Call for Papers: The 7th International Conference for Internet Technology and Secured Transactions (ICITST-2012)!   y.zhao at icitst.org
• [Agda] SSMBio 2012: call for participation   GRLMC
• [Agda] help with math symbols   Serge D. Mechveliani
  • [Agda] help with math symbols   Jean-Philippe Bernardy
    • [Agda] help with math symbols   Serge D. Mechveliani
  • [Agda] help with math symbols   Dominique Devriese
    • [Agda] help with math symbols   Dominique Devriese
      • [Agda] help with math symbols   Serge D. Mechveliani
      • [Agda] help with math symbols   Dominique Devriese
      • [Agda] help with math symbols   Nils Anders Danielsson
  • [Agda] help with math symbols   Nils Anders Danielsson
• [Agda] ICFP 2012: Second call for participation   Wouter Swierstra
• [Agda] ICFP 2012: Second call for participation   Wouter Swierstra
• [Agda] help with math symbols   Serge D. Mechveliani
  • [Agda] help with math symbols   Dominique Devriese
  • [Agda] help with math symbols   Guillaume Brunerie
  • [Agda] help with math symbols   Serge D. Mechveliani
    • [Agda] help with math symbols   Nils Anders Danielsson
      • [Agda] help with math symbols   Serge D. Mechveliani
      • [Agda] help with math symbols   Nils Anders Danielsson
• [Agda] Bin._<_   Serge D. Mechveliani
  • [Agda] Bin._<_   James Deikun
    • [Agda] Bin._<_   James Deikun
      • [Agda] Bin._<_   Andreas Abel
      • [Agda] Bin._<_   Nils Anders Danielsson
    • [Agda] Bin._<_   Serge D. Mechveliani
      • [Agda] Bin._<_   James Deikun
  • [Agda] Bin._<_   Nils Anders Danielsson
• [Agda] Installing Agda   Jason Gross
  • [Agda] Installing Agda   Andreas Abel
    • [Agda] Installing Agda   Jason Gross
      • [Agda] Installing Agda   Nils Anders Danielsson
      • [Agda] Installing Agda   Jason Gross
• [Agda] Call for Participation: Implementation and Application of Functional Languages 2012   Tom Harper
• [Agda] TPNC 2012: 2nd call for posters   GRLMC
• [Agda] GAMES 2012 -- Call for participation --   Nello Murano
• [Agda] Building Agda with newer haskeline   Dirk Ullrich
  • [Agda] Building Agda with newer haskeline   Nils Anders Danielsson
• [Agda] GandALF 2012 -- Call for participation --   Nello Murano
• [Agda] equality on Integer   Serge D. Mechveliani
  • [Agda] equality on Integer   Nils Anders Danielsson
• [Agda] class inheritance   Serge D. Mechveliani
  • [Agda] class inheritance   Nils Anders Danielsson
• [Agda] FSFLA 2012: 3rd announcement   GRLMC
• [Agda] LATA 2013: 1st call for papers   GRLMC
• [Agda] simple example   Serge D. Mechveliani
  • [Agda] simple example   Serge D. Mechveliani
  • [Agda] simple example   Nils Anders Danielsson
    • [Agda] simple example   Serge D. Mechveliani
• [Agda] simple example   Dan Rosén
  • [Agda] simple example   Serge D. Mechveliani
    • Switching off termination checker [Re: [Agda] simple example]   Andreas Abel
      • Switching off termination checker [Re: [Agda] simple example]   Serge D. Mechveliani
• [Agda] CFP: Systems Software Verification (SSV'12)   Gerwin Klein
• [Agda] simple example   Dan Rosén
• [Agda] TPNC 2012: final call for posters   GRLMC
• [Agda] Strictly positive types   Andrés Sicard-Ramírez
  • [Agda] Strictly positive types   Nils Anders Danielsson
    • [Agda] Strictly positive types   Andrés Sicard-Ramírez
      • [Agda] Strictly positive types   Nils Anders Danielsson
      • [Agda] Strictly positive types   Andrés Sicard-Ramírez
• [Agda] on `data' syntax   Serge D. Mechveliani
  • [Agda] on `data' syntax   Nils Anders Danielsson
• [Agda] IEEE HLDVT 2012: Call for Work-in-Progress Abstracts (Deadline: August 27, 2012)   Hiren D. Patel
• [Agda] \exists definition   Serge D. Mechveliani
  • [Agda] \exists definition   Serge D. Mechveliani
    • [Agda] \exists definition   Daniel Peebles
• [Agda] `postulate' in `let'   Serge D. Mechveliani
  • [Agda] `postulate' in `let'   Nils Anders Danielsson
• [Agda] [REMINDER] Agda Intensive Meeting 16th (AIM XVI) in Copenhagen   Nicolas Pouillard
  • [yoshiki] [Agda] [REMINDER] Agda Intensive Meeting 16th (AIM XVI) in Copenhagen   Rika T. Gotoh
• [Agda] record with proof   Serge D. Mechveliani
  • [Agda] record with proof   Serge D. Mechveliani
• [Agda] FSNC 2012: 1st announcement   GRLMC
• [Agda] Typed vs untyped lambda abstractions   Guillaume Brunerie
  • [Agda] Typed vs untyped lambda abstractions   Paul van der Walt
  • [Agda] Typed vs untyped lambda abstractions   wren ng thornton
  • [Agda] Typed vs untyped lambda abstractions   Andreas Abel
    • [Agda] Typed vs untyped lambda abstractions   Thierry Coquand
      • [Agda] Typed vs untyped lambda abstractions   Vladimir Voevodsky
      • [Agda] Typed vs untyped lambda abstractions   Andreas Abel
      • [Agda] Typed vs untyped lambda abstractions   Andreas Abel
• [Agda] `case' vs `with'   Serge D. Mechveliani
  • [Agda] `case' vs `with'   Nils Anders Danielsson
• [Agda] Semigroup declaration   Serge D. Mechveliani
• [Agda] Final Call for Papers, Extended Abstracts and Posters: Ireland International Conference on Education (IICE-2012)!   Margaret Smith
• [Agda] Semigroup declaration   Dan Rosén
  • [Agda] Semigroup declaration   Serge D. Mechveliani
• [Agda] JS compiler - normalization   Станислав Черничкин
  • [Agda] JS compiler - normalization   Andreas Abel
    • [Agda] JS compiler - normalization   Alan Jeffrey
• [Agda] [TYPES/announce] IAS program wiki   Vladimir Voevodsky
• [Agda] `where' in type   Serge D. Mechveliani
  • [Agda] `where' in type   Andreas Abel
• [Agda] _$_   Serge D. Mechveliani
  • [Agda] _$_   Nils Anders Danielsson
  • [Agda] _$_   Serge D. Mechveliani
    • [Agda] _$_   Nils Anders Danielsson
• [Agda] ANN: Jekejeke Prolog 0.9.5 (runtime console, google play)   Jan Burse
  • [Agda] ANN: Jekejeke Prolog 0.9.5 (runtime console, google play)   Andreas Abel
    • [Agda] Re: ANN: Jekejeke Prolog 0.9.5 (runtime console, google play)   Jan Burse
• [Agda] Call for Lightning Talks / Challenges, Workshop on Generic Programming 2012   Andres Löh
• [Agda] _divMod_   Serge D. Mechveliani
  • [Agda] _divMod_   Andreas Abel
• [Agda] TLCA 2013 First Call for Papers   Luca Paolini
• [Agda] Data.Vec.Equality.PropositionalEquality should publish _\~=_   Helmut Grohne
• [Agda] message of parameterized   Serge D. Mechveliani
  • [Agda] message of parameterized   Andreas Abel
    • [Agda] message of parameterized   Serge D. Mechveliani
      • [Agda] message of parameterized   Nils Anders Danielsson
• [Agda] Forget Hurken's Paradox, Agda has a quicker route to success   Andreas Abel
  • [Agda] Forget Hurken's Paradox, Agda has a quicker route to success   Nils Anders Danielsson
    • [Agda] Forget Hurken's Paradox, Agda has a quicker route to success   Andreas Abel
      • [Agda] Forget Hurken's Paradox, Agda has a quicker route to success   Andrés Sicard-Ramírez
      • [Agda] Forget Hurken's Paradox, Agda has a quicker route to success   Andreas Abel
    • [Agda] Forget Hurken's Paradox, Agda has a quicker route to success   Dan Doel
      • [Agda] Forget Hurken's Paradox, Agda has a quicker route to success   Altenkirch Thorsten
      • [Agda] Forget Hurken's Paradox, Agda has a quicker route to success   Andreas Abel
• [Agda] Agdas constraint solver too eager?!   Andreas Abel
  • [Agda] Agdas constraint solver too eager?!   Nils Anders Danielsson
  • [Agda] Agdas constraint solver too eager?!   Andreas Abel
    • [Agda] Agdas constraint solver too eager?!   Gabriel Scherer
      • [Agda] Agdas constraint solver too eager?!   Andreas Abel
    • [Agda] Agdas constraint solver too eager?!   James Deikun
      • [Agda] Agdas constraint solver too eager?!   Andreas Abel
      • Phantom arguments [Re: [Agda] Agdas constraint solver too eager?!]   Andreas Abel
    • [Agda] Agdas constraint solver too eager?!   James Deikun
      • [Agda] Agdas constraint solver too eager?!   Andreas Abel
      • [Agda] Agdas constraint solver too eager?!   James Deikun
      • [Agda] Agdas constraint solver too eager?!   Andreas Abel
  • [Agda] Agdas constraint solver too eager?!   Ulf Norell
    • [Agda] Agdas constraint solver too eager?!   Ulf Norell
    • [Agda] Agdas constraint solver too eager?!   Nils Anders Danielsson
    • [Agda] Agdas constraint solver too eager?!   Andreas Abel
• [Agda] Book Announcement   Gopalan Nadathur
• [Agda] congruence, Preserves_2   Serge D. Mechveliani
  • [Agda] congruence, Preserves_2   Serge D. Mechveliani
    • [Agda] congruence, Preserves_2   Andreas Abel
  • [Agda] congruence, Preserves_2   Andreas Abel
    • [Agda] congruence, Preserves_2   Serge D. Mechveliani
• [Agda] TPNC 2012: call for participation   GRLMC
• [Agda] LATA 2013: 2nd call for papers   URV - RESEARCH GROUP ON MATHEMATICAL LINGUISTICS
• [Agda] ACM SAC 2013 - CFP Programming for Separation of Concerns Track   Emiliano Tramontana
• [Agda] monot-minus for Nat   Serge D. Mechveliani
  • [Agda] monot-minus for Nat   Serge D. Mechveliani
  • [Agda] monot-minus for Nat   Nils Anders Danielsson
    • [Agda] monot-minus for Nat   Serge D. Mechveliani
      • [Agda] monot-minus for Nat   Nils Anders Danielsson
• [Agda] Compiling Standard Library with GHC 7.6   Dirk Ullrich
  • [Agda] Compiling Standard Library with GHC 7.6   Lyndon Maydwell
    • [Agda] Compiling Standard Library with GHC 7.6   Andrés Sicard-Ramírez
    • [Agda] Compiling Standard Library with GHC 7.6   Nils Anders Danielsson
      • [Agda] Compiling Standard Library with GHC 7.6   Lyndon Maydwell
• [Agda] divMod variant   Serge D. Mechveliani
• [Agda] FSNC 2012: 2nd announcement   GRLMC
• [Agda] LICS 2013 - Call for Papers   Andrzej Murawski
  • [Agda] Second Call for Papers: BEAT'13 - 1st International Workshop on Behavioural Types   Hans Hüttel
• [Agda] Standard library patch for newest darcs version of Agda   Andreas Abel
• [Agda] indices in record   Serge D. Mechveliani
  • Parsing telescopes [Re: [Agda] indices in record]   Andreas Abel
• [Agda] deadline extension: Systems Software Verification (SSV'12)   Gerwin Klein
• [Agda] Seeking Pointers for an Introductory Presentation   Lyndon Maydwell
  • [Agda] Seeking Pointers for an Introductory Presentation   Joachim Breitner
    • [Agda] Seeking Pointers for an Introductory Presentation   Andreas Abel
    • [Agda] Seeking Pointers for an Introductory Presentation   Nils Anders Danielsson
  • [Agda] Seeking Pointers for an Introductory Presentation   Andreas Abel
• [Agda] tuple patterns   Serge D. Mechveliani
  • [Agda] tuple patterns   Nils Anders Danielsson
    • [Agda] tuple patterns   Serge D. Mechveliani
      • [Agda] tuple patterns   Nils Anders Danielsson
      • [Agda] tuple patterns   Serge D. Mechveliani
      • [Agda] tuple patterns   Alan Jeffrey
• [Agda] termination proofs   Serge D. Mechveliani
  • [Agda] termination proofs   gallais at ensl.org
    • [Agda] termination proofs   Serge D. Mechveliani
      • [Agda] termination proofs   Sanjoy Das
      • [Agda] termination proofs   Nils Anders Danielsson
      • [Agda] termination proofs   Serge D. Mechveliani
      • [Agda] termination proofs   Altenkirch Thorsten
      • [Agda] termination proofs   Jacques Carette
      • [Agda] termination proofs   Altenkirch Thorsten
      • [Agda] termination proofs   Jacques Carette
      • [Agda] termination proofs   Peter Hancock
      • [Agda] termination proofs   Martin Escardo
      • [Agda] termination proofs   Altenkirch Thorsten
      • [Agda] termination proofs   Peter Hancock
      • [Agda] termination proofs   Serge D. Mechveliani
      • [Agda] termination proofs   Peter Hancock
      • [Agda] termination proofs   Serge D. Mechveliani
      • [Agda] termination proofs   Peter Hancock
      • [Agda] termination proofs   Altenkirch Thorsten
• [Agda] constant evaluation   Serge D. Mechveliani
• [Agda] Agda compile failure on GHC 7.4   Dominique Devriese
  • [Agda] Agda compile failure on GHC 7.4   Nils Anders Danielsson
    • [Agda] Agda compile failure on GHC 7.4   Dominique Devriese
• [Agda] `where' scope   Serge D. Mechveliani
  • [Agda] `where' scope   Andreas Abel
    • [Agda] `where' scope   Serge D. Mechveliani
    • [Agda] `where' scope   Nils Anders Danielsson
• [Agda] Termination checking: valid or invalid   Wojciech Jedynak
  • Compositional termination [Re: [Agda] Termination checking: valid or invalid]   Andreas Abel
• [Agda] `where' scope   Serge D. Mechveliani
  • [Agda] `where' scope   Cezar Ionescu
• [Agda] PEPM 2013: Final Call for Papers   Shin-Cheng Mu
• [Agda] Compositional termination   Karn Kallio
• [Agda] local needs override   Serge D. Mechveliani
• [Agda] Does the order of patterns matter?   Achim Jung
  • [Agda] Does the order of patterns matter?   Altenkirch Thorsten
    • [Agda] Does the order of patterns matter?   Martin Escardo
      • [Agda] Does the order of patterns matter?   Altenkirch Thorsten
      • [Agda] Does the order of patterns matter?   Martin Escardo
      • [Agda] Does the order of patterns matter?   Altenkirch Thorsten
      • [Agda] Does the order of patterns matter?   Martin Escardo
      • [Agda] Does the order of patterns matter?   Altenkirch Thorsten
      • [Agda] Does the order of patterns matter?   Martin Escardo
      • [Agda] Does the order of patterns matter?   Altenkirch Thorsten
      • [Agda] Does the order of patterns matter?   Dan Licata
      • [Agda] Does the order of patterns matter?   Martin Escardo
      • [Agda] Does the order of patterns matter?   Martin Escardo
      • [Agda] Does the order of patterns matter?   Dan Doel
      • [Agda] Does the order of patterns matter?   Altenkirch Thorsten
      • [Agda] Does the order of patterns matter?   Nils Anders Danielsson
      • [Agda] Does the order of patterns matter?   Andreas Abel
      • [Agda] Does the order of patterns matter?   Altenkirch Thorsten
      • [Agda] Does the order of patterns matter?   Andreas Abel
      • [Agda] Does the order of patterns matter?   Martin Escardo
      • [Agda] Does the order of patterns matter?   Nils Anders Danielsson
      • [Agda] Does the order of patterns matter?   Nils Anders Danielsson
  • [Agda] Does the order of patterns matter?   Nils Anders Danielsson
• [Agda] RTA 2013: First Call for Papers   Sophie Tison
• [Agda] PEPM 2013: Deadline Extension   Shin-Cheng Mu
• [Agda] FSFLA 2012: final announcement   GRLMC
• [Agda] evaluation in compilation   Serge D. Mechveliani
  • [Agda] evaluation in compilation   Nils Anders Danielsson
    • [Agda] evaluation in compilation   Serge D. Mechveliani
      • [Agda] evaluation in compilation   Nils Anders Danielsson
      • [Agda] evaluation in compilation   Serge D. Mechveliani
      • [Agda] evaluation in compilation   Nils Anders Danielsson
  • [Agda] evaluation in compilation   Andreas Abel
    • [Agda] evaluation in compilation   Serge D. Mechveliani
      • [Agda] evaluation in compilation   Nils Anders Danielsson
      • [Agda] evaluation in compilation   Serge D. Mechveliani
      • [Agda] evaluation in compilation   Andreas Abel
      • [Agda] evaluation in compilation   Andreas Abel
      • [Agda] evaluation in compilation   Serge D. Mechveliani
      • [Agda] evaluation in compilation   Andreas Abel
      • [Agda] evaluation in compilation   Serge D. Mechveliani
  • [Agda] evaluation in compilation   Serge D. Mechveliani
    • [Agda] evaluation in compilation   Nils Anders Danielsson
      • [Agda] evaluation in compilation   Serge D. Mechveliani
      • [Agda] evaluation in compilation   Nils Anders Danielsson
• [Agda] PLPV 2013 Last Call for Papers   Andreas Abel
• [Agda] readFile and output   Serge D. Mechveliani
  • [Agda] readFile and output   Serge D. Mechveliani
    • [Agda] readFile and output   Nils Anders Danielsson
• [Agda] Colist -> List   Serge D. Mechveliani
  • [Agda] Colist -> List   Daniel Peebles
    • [Agda] Colist -> List   Andreas Abel
      • [Agda] Colist -> List   Nils Anders Danielsson
• [Agda] Re: Colist -> List   Karn Kallio
• [Agda] type of map..<=   Serge D. Mechveliani
  • [Agda] type of map..<=   Sanjoy Das
    • [Agda] type of map..<=   Serge D. Mechveliani
      • [Agda] type of map..<=   Sanjoy Das
• [Agda] LICS 2013 - Call for Workshop Proposals   Andrzej Murawski
• [Agda] syntax highlighting   Martin Escardo
  • [Agda] syntax highlighting   Francesco Mazzoli
    • [Agda] syntax highlighting   Martin Escardo
  • [Agda] syntax highlighting   Nils Anders Danielsson
• [Agda] Date of AIM XVII fixed: 2013.5.8 - 5.14   KINOSHITA Yoshiki
• [Agda] @-patterns   Serge D. Mechveliani
  • [Agda] @-patterns   Daniel Peebles
  • [Agda] @-patterns   Daniel Peebles
    • [Agda] @-patterns   Serge D. Mechveliani
• [Agda] SR 2013 - Preliminary call for contributions   Nello Murano
• [Agda] type of map..<=   Dan Rosén
• [Agda] proof run time cost   Serge D. Mechveliani
  • [Agda] proof run time cost   Andreas Abel
    • [Agda] proof run time cost   Serge D. Mechveliani
• [Agda] FSNC 2012: 3rd announcement   GRLMC
• [Agda] direct product for list   Serge D. Mechveliani
  • [Agda] direct product for list   Andreas Abel
    • [Agda] direct product for list   Serge D. Mechveliani
      • [Agda] direct product for list   Andreas Abel
      • [Agda] direct product for list   Serge D. Mechveliani
      • [Agda] direct product for list   Andreas Abel
• [Agda] generic type recursion   Serge D. Mechveliani
  • [Agda] generic type recursion   Daniel Peebles
    • [Agda] generic type recursion   Serge D. Mechveliani
• [Agda] `using (DecTotalOrder)'   Serge D. Mechveliani
  • [Agda] `using (DecTotalOrder)'   Dominique Devriese
    • [Agda] `using (DecTotalOrder)'   Serge D. Mechveliani
      • [Agda] `using (DecTotalOrder)'   Nils Anders Danielsson
• [Agda] `let' in record decl   Serge D. Mechveliani
  • [Agda] `let' in record decl   Andreas Abel
    • [Agda] `let' in record decl   Serge D. Mechveliani
• [Agda] Sharing --- Q-combinators   Wolfram Kahl
  • [Agda] Sharing --- Q-combinators   Andreas Abel
    • [Agda] Sharing --- Q-combinators   Peter Divianszky
      • [Agda] Sharing --- Q-combinators   Andreas Abel
      • [Agda] Sharing --- Q-combinators   Peter Divianszky
      • [Agda] Sharing --- Q-combinators   Andreas Abel
      • [Agda] Sharing --- Q-combinators   Andreas Abel
• [Agda] `let' in record decl   Serge D. Mechveliani
  • [Agda] `let' in record decl   Nicolas Pouillard
    • [Agda] `let' in record decl   Nils Anders Danielsson
      • [Agda] `let' in record decl   Andreas Abel
      • [Agda] `let' in record decl   Nils Anders Danielsson
      • Let in telescopes, where to put the color? [Re: [Agda] `let' in record decl]   Andreas Abel
      • Let in telescopes, where to put the color? [Re: [Agda] `let' in record decl]   Nils Anders Danielsson
      • Let in telescopes, where to put the color? [Re: [Agda] `let' in record decl]   Nicolas Pouillard
      • Let in telescopes, where to put the color? [Re: [Agda] `let' in record decl]   Andreas Abel
      • Let in telescopes, where to put the color? [Re: [Agda] `let' in record decl]   Nicolas Pouillard
      • [Agda] `let' in record decl   Andreas Abel
• [Agda] Total: x !<= y ==> y <= x   Serge D. Mechveliani
  • [Agda] Total: x !<= y ==> y <= x   Daniel Peebles
• [Agda] Sharing --- Q-combinators   wren ng thornton
  • [Agda] Sharing --- Q-combinators   Wolfram Kahl
• [Agda] Total: x !<= y ==> y <= x   wren ng thornton
  • [Agda] Total: x !<= y ==> y <= x   Serge D. Mechveliani
    • [Agda] Total: x !<= y ==> y <= x   Andrés Sicard-Ramírez
      • [Agda] Total: x !<= y ==> y <= x   Serge D. Mechveliani
      • [Agda] Total: x !<= y ==> y <= x   Nils Anders Danielsson
    • [Agda] Total: x !<= y ==> y <= x   Serge D. Mechveliani
• [Agda] Building Agda with ghc-6.12.3: build failure on geniplate   Guillaume Brunerie
  • [Agda] Re: Building Agda with ghc-6.12.3: build failure on geniplate   Guillaume Brunerie
  • [Agda] Building Agda with ghc-6.12.3: build failure on geniplate   Nils Anders Danielsson
    • [Agda] Building Agda with ghc-6.12.3: build failure on geniplate   Guillaume Brunerie
• [Agda] `let' in record decl   Andreas Abel
  • [Agda] `let' in record decl   Serge D. Mechveliani
    • [Agda] `let' in record decl   Andreas Abel
    • [Agda] `let' in record decl   Nicolas Pouillard
• [Agda] Indentation for abstract and private declarations   Guillaume Brunerie
  • [Agda] Indentation for abstract and private declarations   Andreas Abel
  • [Agda] Indentation for abstract and private declarations   Wolfram Kahl
• [Agda] Building Agda with ghc-6.12.3: build failure on geniplate   Dan Rosén
  • [Agda] Building Agda with ghc-6.12.3: build failure on geniplate   James Chapman
    • [Agda] Building Agda with ghc-6.12.3: build failure on geniplate   Guillaume Brunerie
• [Agda] unused bindings   Serge D. Mechveliani
• [Agda] moving common from `with'   Serge D. Mechveliani
  • [Agda] moving common from `with'   Andreas Abel
    • [Agda] moving common from `with'   Serge D. Mechveliani
      • [Agda] moving common from `with'   Andreas Abel
      • [Agda] moving common from `with'   Serge D. Mechveliani
      • [Agda] moving common from `with'   Dan Doel
      • [Agda] moving common from `with'   Andreas Abel
      • [Agda] moving common from `with'   Dan Doel
• [Agda] Agda Unique type   Dmytro Starosud
  • [Agda] Agda Unique type   Nils Anders Danielsson
    • [Agda] Agda Unique type   Dmytro Starosud
• [Agda] Fairbairn not for St.lib   Serge D. Mechveliani
  • [Agda] Fairbairn not for St.lib   Nils Anders Danielsson
    • [Agda] Fairbairn not for St.lib   Serge D. Mechveliani
  • [Agda] Fairbairn not for St.lib   Wolfram Kahl
• [Agda] Seg-fault   Serge D. Mechveliani
  • [Agda] Seg-fault   Nils Anders Danielsson
    • [Agda] Seg-fault   Wolfram Kahl
    • [Agda] Seg-fault   Serge D. Mechveliani
      • [Agda] Seg-fault   Serge D. Mechveliani
• [Agda] lists/vectors   Amr Sabry
  • [Agda] lists/vectors   Andrés Sicard-Ramírez
    • [Agda] lists/vectors   Amr Sabry
      • [Agda] lists/vectors   Dominique Devriese
      • [Agda] lists/vectors   Noam Zeilberger
    • [Agda] lists/vectors (interfacing with untrusted code)   Amr Sabry
      • [Agda] lists/vectors (interfacing with untrusted code)   gallais at ensl.org
      • [Agda] lists/vectors (interfacing with untrusted code)   Amr Sabry
      • [Agda] lists/vectors (interfacing with untrusted code)   gallais at ensl.org
      • [Agda] lists/vectors (interfacing with untrusted code)   Amr Sabry
      • [Agda] lists/vectors (interfacing with untrusted code)   Nils Anders Danielsson
  • [Agda] lists/vectors   Nils Anders Danielsson
    • [Agda] lists/vectors   Amr Sabry
      • [Agda] lists/vectors   Nils Anders Danielsson
• [Agda] LATA 2013: 3rd call for papers   GRLMC
• [Agda] `syntax'   Serge D. Mechveliani
  • [Agda] `syntax'   Nils Anders Danielsson
    • [Agda] `syntax'   Serge D. Mechveliani
      • [Agda] `syntax'   Daniel Peebles
      • [Agda] `syntax'   Nils Anders Danielsson
• [Agda] lists/vectors   Dominique Devriese
• [Agda] parameterized modules?   Serge D. Mechveliani
  • [Agda] parameterized modules?   Andreas Abel
    • [Agda] parameterized modules?   Serge D. Mechveliani
      • [Agda] parameterized modules?   Andreas Abel
• [Agda] Some module statements, for your amusement   Andreas Abel
  • Replacement of 'as' in module statements? [Re: [Agda] Some module statements, for your amusement]   Andreas Abel
    • [Agda] Re: Replacement of 'as' in module statements?   Nils Anders Danielsson
      • [Agda] Re: Replacement of 'as' in module statements?   Andreas Abel
      • [Agda] Re: Replacement of 'as' in module statements?   Nils Anders Danielsson
      • [Agda] Re: Replacement of 'as' in module statements?   Andreas Abel
      • [Agda] Re: Replacement of 'as' in module statements?   Nils Anders Danielsson
• [Agda] laziness damaged   Serge D. Mechveliani
  • [Agda] laziness damaged   Jeffrey, Alan S A (Alan)
    • [Agda] laziness damaged   Serge D. Mechveliani
• [Agda] CfP: Enabling Domain Experts to use Formalised Reasoning@AISB 2013 (Exeter, UK, 2-5 Apr 2013); Deadlines 10 Dec and 14 Jan   Christoph LANGE
• [Agda] 5 sec performance gain on std-lib   Andreas Abel
• [Agda] 5 sec performance gain on std-lib   James Chapman
  • [Agda] 5 sec performance gain on std-lib   Andreas Abel
• [Agda] Agda pragmas are rendered incorrectly in lhs2tex   Andrés Sicard-Ramírez
  • [Agda] Agda pragmas are rendered incorrectly in lhs2tex   Andreas Abel
    • [Agda] Agda pragmas are rendered incorrectly in lhs2tex   Andrés Sicard-Ramírez
• [Agda] DTO, STO, AVL.Tree   Serge D. Mechveliani
  • [Agda] DTO, STO, AVL.Tree   Nils Anders Danielsson
    • [Agda] DTO, STO, AVL.Tree   Serge D. Mechveliani
• [Agda] WSLST 2013: 1st announcement   GRLMC
• [Agda] Emacs with dark background and Agdan   Francesco Mazzoli
  • [Agda] Re: Emacs with dark background and Agdan   Francesco Mazzoli
  • [Agda] Emacs with dark background and Agdan   Nils Anders Danielsson
• [Agda] CFP: Term and Graph Rewriting (TERMGRAPH2013) / ETAPS2013   Wolfram Kahl
• [Agda] ICFP 2013: Call for workshops and co-located events   David Van Horn
• [Agda] How to avoid T3 fonts in pdf generated with lhs2TeX?   Andreas Abel
  • [Agda] How to avoid T3 fonts in pdf generated with lhs2TeX?   Dominique Devriese
  • [Agda] How to avoid T3 fonts in pdf generated with lhs2TeX?   Dominique Devriese
    • [Haskell-cafe] [Agda] How to avoid T3 fonts in pdf generated with lhs2TeX?   Andreas Abel
  • [Agda] How to avoid T3 fonts in pdf generated with lhs2TeX?   Andrés Sicard-Ramírez
  • [Agda] How to avoid T3 fonts in pdf generated with lhs2TeX?   Nils Anders Danielsson
• [Agda] Understanding productivity   Daniel Peebles
  • [Agda] Understanding productivity   Andreas Abel
  • [Agda] Understanding productivity   Nils Anders Danielsson
• [Agda] Mac OS 10.6 Emacs 24.2 and unicode   Andreas Abel
• [Agda] LATA 2013: submission deadline extended   GRLMC
• [Agda] partial division property   Serge D. Mechveliani
  • [Agda] partial division property   Nils Anders Danielsson
    • [Agda] partial division property   Serge D. Mechveliani
      • [Agda] partial division property   Nils Anders Danielsson
  • [Agda] partial division property   Serge D. Mechveliani
• [Agda] windows installer is not available   Peter Divianszky
  • [Agda] Re: windows installer is not available   Peter Divianszky
    • [Agda] Re: windows installer is not available   Darius Jahandarie
      • [Agda] Re: windows installer is not available   Makoto Takeyama
      • [Agda] Re: windows installer is not available   Makoto Takeyama
      • [Agda] Re: windows installer is not available   Peter Divianszky
• [Agda] on "Dependently Typed.."   Serge D. Mechveliani
  • [Agda] on "Dependently Typed.."   Andreas Abel
    • [Agda] on "Dependently Typed.."   James Chapman
• [Agda] boundings in data-where   Serge D. Mechveliani
  • [Agda] boundings in data-where   Serge D. Mechveliani
  • Syntax of 'data' declaration [Re: [Agda] boundings in data-where]   Andreas Abel
    • Syntax of 'data' declaration [Re: [Agda] boundings in data-where]   Serge D. Mechveliani
      • Syntax of 'data' declaration [Re: [Agda] boundings in data-where]   Andreas Abel
• [Agda] skipped ambiguity?   Serge D. Mechveliani
  • [Agda] skipped ambiguity?   Andreas Abel
• [Agda] data syntax ext.   Serge D. Mechveliani
• [Agda] Decidable _\~~_ of Semiring   Serge D. Mechveliani
  • [Agda] Decidable _\~~_ of Semiring   Andreas Abel
    • [Agda] Decidable _\~~_ of Semiring   Serge D. Mechveliani
      • [Agda] Decidable _\~~_ of Semiring   Daniel Peebles
      • [Agda] Decidable _\~~_ of Semiring   Serge D. Mechveliani
      • [Agda] Decidable _\~~_ of Semiring   Daniel Peebles
      • [Agda] Decidable _\~~_ of Semiring   Serge D. Mechveliani
      • [Agda] Decidable _\~~_ of Semiring   Serge D. Mechveliani
• [Agda] SR 2013 - Call for contributions   Nello Murano
• [Agda] `data'-record field overlap   Serge D. Mechveliani
  • [Agda] Re: `data'-record field overlap   Francesco Mazzoli
    • [Agda] Re: `data'-record field overlap   Francesco Mazzoli
      • [Agda] Re: `data'-record field overlap   Andreas Abel
  • [Agda] `data'-record field overlap   Andreas Abel
• [Agda] CFP : 2nd International Workshop on Engineering Safety and Security Systems (ESSS)   =?Big5?B?pHOnzr/gpKc=?=
• [Agda] Announce: Agda 2.3.2   Andreas Abel
• [Agda] Announce: Agda 2.3.2   Andreas Abel
• [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   raichoo
  • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   Cezar Ionescu
    • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   Andreas Abel
  • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   Andrés Sicard-Ramírez
    • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   Cezar Ionescu
      • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   Andrés Sicard-Ramírez
      • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   Nils Anders Danielsson
      • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   Cezar Ionescu
      • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   Nils Anders Danielsson
      • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   Andrés Sicard-Ramírez
      • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   Andrés Sicard-Ramírez
      • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   Andreas Abel
      • [Agda] Important: Remove mtl-2.1 from your system!!   Andreas Abel
      • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   Cezar Ionescu
      • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   raichoo
      • [Agda] Problems with emacs agda-mode after upgrading to 2.3.2   Nils Anders Danielsson
• [Agda] Positivity check   Andrew Cave
  • [Agda] Positivity check   Andreas Abel
    • [Agda] Positivity check   Daniel Peebles
    • [Agda] Positivity check   Andrew Cave
• [Agda] Unification assumes injective postulates?   Jan Malakhovski
  • [Agda] Unification assumes injective postulates?   Andrés Sicard-Ramírez
  • [Agda] Unification assumes injective postulates?   Nils Anders Danielsson
    • [Agda] Unification assumes injective postulates?   Andreas Abel
      • [Agda] Unification assumes injective postulates?   Dominique Devriese
      • [Agda] Unification assumes injective postulates?   Dan Licata
      • [Agda] Unification assumes injective postulates?   Andreas Abel
      • [Agda] Unification assumes injective postulates?   Jan Malakhovski
      • [Agda] Unification assumes injective postulates?   Nils Anders Danielsson
      • [Agda] Unification assumes injective postulates?   Jan Malakhovski
      • [Agda] Unification assumes injective postulates?   Nils Anders Danielsson
• Fw: Re: [Agda] Unification assumes injective postulates?   Jan Malakhovski
• [Agda] Application for PhD Studentship   Kuttuvam Meeyakhan KhanMohamed
• [Agda] Building utilities for Agda?   Darryl
  • [Agda] Building utilities for Agda?   Andreas Abel
  • [Agda] Building utilities for Agda?   Nils Anders Danielsson
• [Agda] Two papers on Agda and FRP   Alan Jeffrey
  • [Agda] Two papers on Agda and FRP   Andreas Abel
• [Agda] Question about the meaning of 'abstract'   Andreas Abel
  • [Agda] Question about the meaning of 'abstract'   Daniel Peebles
    • [Agda] Question about the meaning of 'abstract'   Daniel Peebles
• [Agda] Question about the meaning of 'abstract'   Dan Licata
  • [Agda] Question about the meaning of 'abstract'   Nils Anders Danielsson
    • [Agda] Question about the meaning of 'abstract'   Dan Licata
  • [Agda] Question about the meaning of 'abstract'   Andreas Abel
    • [Agda] Question about the meaning of 'abstract'   Nils Anders Danielsson
• [Agda] with + continuation   Peter Divianszky
  • [Agda] Re: with + continuation   Peter Divianszky
    • [Agda] Re: with + continuation   Andreas Abel
      • [Agda] Re: with + continuation   Peter Divianszky
      • [Agda] Re: with + continuation   Peter Divianszky
      • [Agda] Re: with + continuation   Twan van Laarhoven
      • vertical application (Re: [Agda] Re: with + continuation)   Peter Divianszky
• [Agda] Call for Participation: Programming Languages Mentoring Workshop - a POPL workshop.   Gareth Smith
• [Agda] 2nd CfP: Enabling Domain Experts to use Formalised Reasoning@AISB 2013 (Exeter, UK, 2-5 Apr 2013); Deadlines 10 Dec and 14 Jan   Christoph LANGE
• [Agda] function parameters similar to data parameters   Peter Divianszky
  • [Agda] function parameters similar to data parameters   Dominique Devriese
    • [Agda] function parameters similar to data parameters   Andreas Abel
  • [Agda] function parameters similar to data parameters   Andreas Abel
    • [Agda] function parameters similar to data parameters   Peter Divianszky
      • [Agda] function parameters similar to data parameters   Andreas Abel
      • [Agda] function parameters similar to data parameters   Peter Divianszky
      • [Agda] function parameters similar to data parameters   Nils Anders Danielsson
• [Agda] optional dot in dot patterns?   Peter Divianszky
  • [Agda] optional dot in dot patterns?   Nils Anders Danielsson
    • [Agda] optional dot in dot patterns?   Peter Divianszky
      • [Agda] optional dot in dot patterns?   Nils Anders Danielsson
      • [Agda] optional dot in dot patterns?   Peter Divianszky
      • [Agda] optional dot in dot patterns?   Andreas Abel
      • [Agda] optional dot in dot patterns?   Peter Divianszky
  • [Agda] optional dot in dot patterns?   Dan Doel
    • [Agda] optional dot in dot patterns?   Peter Divianszky
• [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
  • [Agda] Classical Mathematics for a Constructive World   Nils Anders Danielsson
    • [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
      • [Agda] Classical Mathematics for a Constructive World   Jacques Carette
      • [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
  • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
    • [Agda] Re: Classical Mathematics for a Constructive World   Jan Burse
      • [Agda] Re: Classical Mathematics for a Constructive World   Jan Burse
      • [Agda] Re: Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Re: Classical Mathematics for a Constructive World   Liang-Ting Chen
      • [Agda] Re: Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Re: Classical Mathematics for a Constructive World   Altenkirch Thorsten
      • [Agda] Re: Classical Mathematics for a Constructive World   Jan Burse
    • [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   Dan Doel
      • [Agda] Re: Classical Mathematics for a Constructive World   Jan Burse
      • [Agda] Re: Classical Mathematics for a Constructive World   Jan Burse
      • [Agda] Re: Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Re: Classical Mathematics for a Constructive World   Jan Burse
      • [Agda] Re: Classical Mathematics for a Constructive World   Jan Burse
      • [Agda] Classical Mathematics for a Constructive World   Dan Licata
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   Dan Licata
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   wren ng thornton
      • [Agda] Classical Mathematics for a Constructive World   wren ng thornton
      • [Agda] Re: Classical Mathematics for a Constructive World   Jan Burse
      • [Agda] Re: Classical Mathematics for a Constructive World   Ramana Kumar
      • [Agda] Re: Classical Mathematics for a Constructive World   Jan Burse
      • [Agda] Re: Classical Mathematics for a Constructive World   Ramana Kumar
      • [Agda] Re: Classical Mathematics for a Constructive World   Jan Burse
      • [Agda] Re: Classical Mathematics for a Constructive World   wren ng thornton
      • [Agda] Classical Mathematics for a Constructive World   Altenkirch Thorsten
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
      • [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
      • [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
      • [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
      • [Agda] Classical Mathematics for a Constructive World   Andreas Abel
      • [Agda] Re: Classical Mathematics for a Constructive World   Jan Burse
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   Peter Hancock
      • [Agda] Classical Mathematics for a Constructive World   Altenkirch Thorsten
      • [Agda] Classical Mathematics for a Constructive World   Altenkirch Thorsten
      • [Agda] Set levels and library issues   Matthew
      • [Agda] Set levels and library issues   Nils Anders Danielsson
      • [Agda] Classical Mathematics for a Constructive World   Martin Escardo
      • [Agda] Classical Mathematics for a Constructive World   Peter Hancock
      • [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
      • [Agda] Classical Mathematics for a Constructive World   wren ng thornton
      • [Agda] Classical Mathematics for a Constructive World   Peter Hancock
• [Agda] Re: Agda Digest, Vol 87, Issue 24   Valeria de Paiva
  • [Agda] Re: Agda Digest, Vol 87, Issue 24   Martin Escardo
    • [Agda] Re: Agda Digest, Vol 87, Issue 24   Dan Licata
      • [Agda] Re: Agda Digest, Vol 87, Issue 24   Altenkirch Thorsten
      • [Agda] Re: Agda Digest, Vol 87, Issue 24   Dan Licata
• [Agda] ITP 2013: Call for workshop proposals   David Pichardie
• [Agda] Data.Setoid ?   Jacques Carette
  • [Agda] Data.Setoid ?   Wolfram Kahl
• [Agda] agsy extensions   Peter Divianszky
  • [Agda] agsy extensions   Andreas Abel
• [Agda] StdLib additions   Peter Divianszky
  • [Agda] StdLib additions   Daniel Peebles
  • [Agda] StdLib additions   Nils Anders Danielsson
• [Agda] DICE 2013, second call for papers   Simona Ronchi della Rocca
• [Agda] ITP 2013: First Call for Papers   David Pichardie
• [Agda] 10th Annual Conference on Theory and Applications of Models of Computation (TAMC13)   S B Cooper
• [Agda] TLCA 2013 Second Call for Papers   Luca Paolini
• [Agda] CiE 2013: The Nature of Computation, Milan, Italy, July 1-5, 2013   S B Cooper
• [Agda] algebra libraries   Serge D. Mechveliani
  • [Agda] algebra libraries   Nils Anders Danielsson
• [Agda] PLMW: Mentoring at POPL. Second Call for Participation   Gareth Smith
• [Agda] SLSP 2013: 1st call for papers   GRLMC
• [Agda] Conference announcement: "Type Theory, Homotopy Theory and Univalent Foundations"   Nicola Gambino
• [Agda] CiE 2013 in Milan - Awards and 2nd Call for Papers   S B Cooper
• [Agda] RTA 2013: Second Call for Papers   Sophie Tison
• [Agda] PEPM 2013: 2nd Call for Participation   Shin-Cheng Mu
• [Agda] no longer type checks   Martin Escardo
  • [Agda] no longer type checks   Andreas Abel
    • [Agda] no longer type checks   Martin Escardo
      • [Agda] no longer type checks   Justus Matthiesen
      • [Agda] no longer type checks   Martin Escardo
  • [Agda] no longer type checks   Andreas Abel
    • [Agda] no longer type checks   Martin Escardo
      • [Agda] no longer type checks   Peter Hancock
      • Linear Pattern Inductive Famlies [Re: [Agda] no longer type checks]   Andreas Abel
      • Linear Pattern Inductive Famlies [Re: [Agda] no longer type checks]   Gabriel Scherer
      • Linear Pattern Inductive Famlies [Re: [Agda] no longer type checks]   Andreas Abel
    • [Agda] no longer type checks   Nils Anders Danielsson
      • [Agda] no longer type checks   Andreas Abel
      • [Agda] no longer type checks   Nils Anders Danielsson
• [Agda] Patch to build with `hashable-1.2.x'   Dirk Ullrich
  • [Agda] Patch to build with `hashable-1.2.x'   Nils Anders Danielsson
    • [Agda] Patch to build with `hashable-1.2.x'   Dirk Ullrich
• [Agda] Special issue of MSCS: extended deadline   Nicola Gambino
• [Agda] SR 2013 - Extended Deadline and Last Call for Contributions   Nello Murano
• [Agda] CfP: Stage 2 of Enabling Domain Experts to use Formalised Reasoning@AISB 2013 (Exeter, UK, 2-3 Apr 2013); Deadline 14 Jan   Christoph LANGE
• [Agda] LICS 2013 - Last Call for Papers   Andrzej Murawski
• [Agda] PLPV 2013 call for participation   Andreas Abel
• [Agda] Call for papers: Validation of Safety critical Collaboration systems   Andrea Calvagna
• [Agda] Call for Workshops: Conf. Intelligent Computer Mathematics (CICM 2013)   Serge Autexier
• [Agda] CSL 2013 : PRELIMINARY ANNOUNCEMENT   Luca Paolini
• [Agda] CfP: Conf. Intelligent Computer Mathematics (Bath, UK, 7-12 Jul 2013); Deadline 8 Mar   Serge Autexier
• [Agda] proof overhead   Serge D. Mechveliani
  • [Agda] proof overhead   Gabriel Scherer
    • [Agda] proof overhead   Serge D. Mechveliani
• [Agda] ghc for Agda-2.3.2   Serge D. Mechveliani
  • [Agda] Re: ghc for Agda-2.3.2   Francesco Mazzoli
  • [Agda] ghc for Agda-2.3.2   Andreas Abel
• [Agda] Highest Level seen?   Jacques Carette
  • [Agda] Highest Level seen?   Dan Doel
  • [Agda] Highest Level seen?   Darryl
    • [Agda] Highest Level seen?   Jacques Carette
      • [Agda] Highest Level seen?   Darryl
  • [Agda] Highest Level seen?   Nils Anders Danielsson
• [Agda] Semigroup.Carrier in 2.3.2   Serge D. Mechveliani
  • [Agda] Semigroup.Carrier in 2.3.2   Andreas Abel
• [Agda] TAMC 2013 in Hong Kong: Second Call for Papers   S B Cooper
• [Agda] CiE 2013 in Milan - Special Awards and Call for Papers   S B Cooper
• [Agda] ESSS 2013 -- submission deadline extended   =?Big5?B?pHOnzr/gpKc=?=
• [Agda] list member error   Serge D. Mechveliani
  • [Agda] list member error   Andreas Abel
• [Agda] Semigroup.Carrier in 2.3.2   Andreas Abel
  • [Agda] Semigroup.Carrier in 2.3.2   Serge D. Mechveliani
• Issue 777 [Re: [Agda] Semigroup.Carrier in 2.3.2]   Andreas Abel
• Issue 777 [Re: [Agda] Semigroup.Carrier in 2.3.2]   Andreas Abel
• [Agda] arrow symbol   Serge D. Mechveliani

Last message date: Mon Dec 31 18:45:46 CEST 2012
Archived on: Tue Jan 1 08:46:46 CEST 2013

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