2012 Archives by date
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] induction-recursion
wren ng thornton
- [Agda] induction-recursion
Anthony de Almeida Lopes
- [Agda] induction-recursion
wren ng thornton
- [Agda] CICM 2012: Second call for papers
Johan Jeuring
- [Agda] induction-recursion
Nils Anders Danielsson
- [Agda] induction-recursion
Nils Anders Danielsson
- [Agda] Installation problem (Windows 7)
Neil P Strickland
- [Agda] Abstract blocks
Nils Anders Danielsson
- [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] Irrelevance + instance arguments = inconsistency in 2.3.0
Adam Gundry
- [Agda] Irrelevance + instance arguments = inconsistency in 2.3.0
Nils Anders Danielsson
- [Agda] red black trees with delete
Nils Anders Danielsson
- [Agda] Irrelevance + instance arguments = inconsistency in 2.3.0
Andreas Abel
- [Agda] red black trees with delete
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] Irrelevance + instance arguments = inconsistency in 2.3.0
Andreas Abel
- [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] automatically instantiating rewrites
Nils Anders Danielsson
- [Agda] Erasable vs. irrelevant
jleivent at comcast.net
- [Agda] Erasable vs. irrelevant
Andreas Abel
- [Agda] Midlands Graduate School 2012
Altenkirch Thorsten
- [Agda] automatically instantiating rewrites
Ramana Kumar
- [Agda] ITP 2012: Final Call for Papers
Amy Felty
- [Agda] Erasable vs. irrelevant
jleivent at comcast.net
- [Agda] Midlands Graduate School 2012
Altenkirch Thorsten
- [Agda] Turing Centenary Conference (CiE 2012) - Final submission
arrangements
S B Cooper
- [Agda] Erasable vs. irrelevant
Andreas Abel
- [Agda] Erasable vs. irrelevant
jleivent at comcast.net
- [Agda] Erasable vs. irrelevant
Adam Gundry
- [Agda] Erasable vs. irrelevant
Dan Doel
- [Agda] Erasable vs. irrelevant
jleivent at comcast.net
- [Agda] Erasable vs. irrelevant, and red black trees again
jleivent at comcast.net
- [Agda] [PVS] IIP 2012: Call for Papers
liang chang
- [Agda] Erasable vs. irrelevant, and red black trees again
Andreas Abel
- [Agda] Erasable vs. irrelevant, and red black trees again
Adam Gundry
- [Agda] Erasable vs. irrelevant, and red black trees again
Conor McBride
- [Agda] Erasable vs. irrelevant, and red black trees again
Conor McBride
- [Agda] MFPS 28 Second Call for Papers
Ulrich Berger
- [Agda] ITP 2013: Call for bids
Lennart Beringer
- [Agda] Erasable vs. irrelevant, and red black trees again
Alan Jeffrey
- [Agda] Re: Erasable vs. irrelevant
Stefan Monnier
- [Agda] Erasable vs. irrelevant, and red black trees again
Andreas Abel
- [Agda] Re: Erasable vs. irrelevant
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] 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] LATA 2012: call for participation
GRLMC
- [Agda] Asynchronous Emacs mode / Interactive syntax highlighting
Nils Anders Danielsson
- [Agda] WADT 2012: First 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
Andreas Abel
- [Agda] Are there unicorns in Agda?
Martin Escardo
- [Agda] Are there unicorns in Agda?
Vladimir Voevodsky
- [Agda] Call for Papers: International Conference on Information
Society (i-Society 2012)!
Mark Newman
- [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] 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] 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?
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] 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?
Alan Jeffrey
- [Agda] Strange way of displaying \sqcap and \sqcup in emacs 23.3.1
Lubuntu 11.10
Nils Anders Danielsson
- [Agda] Re: Coloring of mixfix identifiers
Nils Anders Danielsson
- [Agda] Strange way of displaying \sqcap and \sqcup in emacs
23.3.1 Lubuntu 11.10
David Wahlstedt
- [Agda] Last CFP FORMAL METHODS 2012
Hanna Klaudel
- [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
- [Agda] Conference on Intelligent Computer Mathematics,
last call for 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
- Erasable Monad (was Re: [Agda] Any examples of monad use in Agda?)
jleivent at comcast.net
- [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] complex indices
Ramana Kumar
- [Agda] complex indices
Ramana Kumar
- [Agda] complex indices
Brandon Moore
- [Agda] complex indices
Andreas Abel
- [Agda] complex indices
Ramana Kumar
- [Agda] complex indices
Ramana Kumar
- [Agda] complex indices
Brandon Moore
- [Agda] complex indices
Andreas Abel
- [Agda] complex indices
Ramana Kumar
- [Agda] Asynchronous Emacs mode / Interactive syntax highlighting
Guilhem Moulin
- [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] ETAPS Workshop on Automation in Proof Assistants (31 Mar - 1
Apr 2012)
Hugo Herbelin
- [Agda] Working with coinductive trees?
Nils Anders Danielsson
- [Agda] Pattern matching order?
Nils Anders Danielsson
- [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] Alan Turing Centenary Conference, University of Manchester,
22-25 June, 2012
S B Cooper
- [Agda] Conversion bug
Nils Anders Danielsson
- [Agda] Working with coinductive trees?
Brandon Moore
- [Agda] CALL FOR PAPERS
Al-mukhatabat Journal
- [Agda] CFP: Workshop on Generic Programming 2012
Andres Loeh
- [Agda] WADT 2012: Second Call for Papers
WADT 2012
- [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] World's biggest fake conference in computer science
James Allen
- [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] 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] Chairman disappears from world's biggest computer conference
James Allen
- [Agda] A demonstration of Agda
Anthony de Almeida Lopes
- [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] TPNC 2012: 2nd call for papers
GRLMC
- [Agda] Recursive Sets / refine vs. load
Nils Anders Danielsson
- [Agda] Recursive Sets / refine vs. load
Altenkirch Thorsten
- [Agda] Wildcards
Guillaume Brunerie
- [Agda] Wildcards
Nils Anders Danielsson
- [Agda] Wildcards
Guillaume Brunerie
- [Agda] Call for Participation: RTA 2012
Georg Moser
- [Agda] Intersection Types and Related Systems (ITRS 2012) -- Final
Call
Luca Paolini
- [Agda] Wildcards
Andreas Abel
- 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] Recursive Sets / refine vs. load
Andreas Abel
- [Agda] Recursive Sets / refine vs. load
Altenkirch Thorsten
- [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
- 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
- [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
- Interleaving typechecking and evaluation [Re: [Agda] Recursive
Sets / refine vs. load]
Andreas Abel
- [Agda] A frontend for the semiring solver using the reflection API
Andreas Abel
- [Agda] WADT 2012: Deadline Extension
WADT 2012
- [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] 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] Conference on Intelligent Computer Mathematics,
call for work-in-progress papers
Johan Jeuring
- [Agda] Short proof of falsity
Anton Setzer
- [Agda] Short proof of falsity
Dan Rosén
- [Agda] Short proof of falsity
Paul van der Walt
- [Agda] Short proof of falsity
Ulf Norell
- [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes
James Deikun
- [Agda] SSNC 2012: 3rd announcement
GRLMC
- [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] 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] 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
- [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes
Nils Anders Danielsson
- Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins
strike again -- Nat is a ring?]
Nils Anders Danielsson
- [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes
James Deikun
- 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?]
Andreas Abel
- [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes
Andreas Abel
- [Agda] interaction interface
Peter Divianszky
- [Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes
Nils Anders Danielsson
- Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins
strike again -- Nat is a ring?]
Nils Anders Danielsson
- [Agda] interaction interface
Ramana Kumar
- [Agda] Parametricity is inconsistent with classical logic
Jean-Philippe Bernardy
- [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: Performance gains for normalization when dumping IO?
James Deikun
- [Agda] Re: strict unit type
Andreas Abel
- [Agda] Re: [TYPES] strict unit type
Altenkirch Thorsten
- [Agda] Parametricity is inconsistent with classical logic
Benja Fallenstein
- [Agda] Parametricity is inconsistent with classical logic
Benja Fallenstein
- [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
- [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
- Re: [Agda] : vs. ∶
Dominique Devriese
- [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] [ANN] Agda Intensive Meeting 16th (AIM XVI) in Copenhagen
Nicolas Pouillard
- [Agda] Bounties for Agda features
Daniel Peebles
- [Agda] Bounties for Agda features
Peter Hancock
- [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
- Unfolding and Rewriting [Re: [Agda] Bounties for Agda features]
Andreas Abel
- [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] Bounties for Agda features
Nils Anders Danielsson
- [Agda] Re: Bounties for Agda features
Thomas Hallgren
- [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?
Jacques Carette
- [Agda] practical integer/rational arithmetic?
Daniel Peebles
- [Agda] practical integer/rational arithmetic?
Nils Anders Danielsson
- [Agda] practical integer/rational arithmetic?
James Deikun
- [Agda] practical integer/rational arithmetic?
Jacques Carette
- [Agda] Strict positivity and indices
Dan Doel
- [Agda] practical integer/rational arithmetic?
Noam Zeilberger
- [Agda] Strict positivity and indices
Nils Anders Danielsson
- [Agda] practical integer/rational arithmetic?
wren ng thornton
- [Agda] Re: [TYPES] strict unit type
Vladimir Voevodsky
- [Agda] Re: strict unit type
Vladimir Voevodsky
- [Agda] Re: strict unit type
Andreas Abel
- [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] 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
Altenkirch Thorsten
- [Agda] Re: [TYPES] strict unit type
Robert Harper
- [Agda] Parametricity is inconsistent with classical logic
Danko Ilik
- [Agda] Re: Strict positivity and indices
Stefan Monnier
- [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] Parametricity is inconsistent with classical logic
Martin Escardo
- [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] 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
Benja Fallenstein
- [Agda] Poll: Mixfix and parametrized modules --- which behavior
would you expect
Gabriel Scherer
- [Agda] Poll: Mixfix and parametrized modules --- which behavior
would you expect
Nils Anders Danielsson
- [Agda] Re: Strict positivity and indices
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] Re: problem using "with"
Nils Anders Danielsson
- [Agda] Weird constraint on type of a record field
Dr. ERDI Gergo
- [Agda] Poll: Mixfix and parametrized modules --- which behavior
would you expect
Dan Doel
- [Agda] Re: problem using "with"
Guillermo Calderón
- [Agda] MFPS 28: Programme and Call for Participation
Ulrich Berger
- [Agda] Poll: Mixfix and parametrized modules --- which behavior
would you expect
Andreas Abel
- [Agda] Re: Strict positivity and indices
Andreas Abel
- [Agda] Weird constraint on type of a record field
Andreas Abel
- [Agda] Re: [Coq-Club] Positivity condition and nested recursion
Andreas Abel
- [Agda] Re: problem using "with"
Nils Anders Danielsson
- [Agda] Re: problem using "with"
Altenkirch Thorsten
- [Agda] Poll: Mixfix and parametrized modules --- which behavior
would you expect
Nils Anders Danielsson
- [Agda] Re: Strict positivity and indices
Nils Anders Danielsson
- [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: Strict positivity and indices
Andreas Abel
- [Agda] Re: problem using "with"
Altenkirch Thorsten
- [Agda] Re: problem using "with"
Guillermo Calderón
- [Agda] Re: problem using "with"
Nils Anders Danielsson
- [Agda] Re: Strict positivity and indices
Ulf Norell
- [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
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] Postulated computing quotients are unsound
Conor McBride
- [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] Poll: Mixfix and parametrized modules --- which behavior
would you expect
Andreas Abel
- [Agda] FSFLA 2012: 1st announcement
GRLMC
- [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] CICM 2012: 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] Re: Your favourite date for AIM XVII (Spring 2013)?
KINOSHITA Yoshiki
- [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] CICM 2012: 2nd Call for participation;
early registration deadline approaching
Johan Jeuring
- [Agda] Absurd pattern; convincing Agda
Paul van der Walt
- [Agda] Influencing pattern matching order [Was: Absurd pattern;
convincing Agda]
Dominique Devriese
- [Agda] Absurd pattern; convincing Agda
Andreas Abel
- [Agda] Absurd pattern; convincing Agda
Daniel Peebles
- [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] Absurd pattern; convincing Agda
Andreas Abel
- [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] expanding solved wildcards
Ramana Kumar
- [Agda] LICS 2012 - Last Call for Participation
Andrzej Murawski
- [Agda] Typechecking a module using Haskell
Lyndon Maydwell
- [Agda] without-K problem
Altenkirch Thorsten
- [Agda] without-K problem
Guillaume Brunerie
- [Agda] ITP2012: call for participation
Lennart Beringer
- [Agda] without-K problem
Andreas Abel
- [Agda] without-K problem
Altenkirch Thorsten
- [Agda] without-K problem
Andreas Abel
- [Agda] More powerful quoting & reflection?
Paul van der Walt
- [Agda] More powerful quoting & reflection?
James Deikun
- [Agda] without-K problem
Nils Anders Danielsson
- [Agda] Agda memory leaks?
Wolfram Kahl
- [Agda] without-K problem
Andreas Abel
- [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] expanding solved wildcards
Nils Anders Danielsson
- [Agda] Bug in ScopeMonad?
Andreas Abel
- [Agda] Bug in ScopeMonad?
Paul van der Walt
- [Agda] FSFLA 2012: 2nd announcement
GRLMC
- [Agda] More powerful quoting & reflection?
Altenkirch Thorsten
- [Agda] ICFP 2012: Call for participation
Wouter Swierstra
- [Agda] CICM 2012: Programme details on-line,
last call for participation
Johan Jeuring
- [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] agda halting problem
Ondrej Rypacek
- [Agda] agda halting problem
Daniel Peebles
- [Agda] agda halting problem
Andreas Abel
- [Agda] agda halting problem
Dan Doel
- [Agda] agda halting problem
Wolfram Kahl
- [Agda] agda halting problem
Andreas Abel
- [Agda] Several open Postdoc Positions at the IT University of
Copenhagen/DemTech
Carsten Schürmann
- [Agda] agda halting problem
Nils Anders Danielsson
- [Agda] agda halting problem
Nils Anders Danielsson
- [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] 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] irrelevant fields and EqReasoning
Noam Zeilberger
- [Agda] Agda for CA
Andreas Abel
- [Agda] irrelevant fields and EqReasoning
Andreas Abel
- [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] irrelevant fields and EqReasoning
Noam Zeilberger
- [Agda] Agda IO - accessing command-line arguments
stvienna wiener
- [Agda] compiling Hello.agda
Serge D. Mechveliani
- [Agda] compiling Hello.agda
James Deikun
- [Agda] compiling Hello.agda
Paul van der Walt
- [Agda] Agda IO - accessing command-line arguments
Andreas Abel
- [Agda] irrelevant fields and EqReasoning
Andreas Abel
- [Agda] compiling Hello.agda
Serge D. Mechveliani
- [Agda] compiling Hello.agda
Andreas Abel
- [Agda] irrelevant fields and EqReasoning
Noam Zeilberger
- [Agda] irrelevant fields and EqReasoning
Jean-Philippe Bernardy
- [Agda] Call for Papers: Ireland International Conference on
Education (IICE-2012)
L inda Woods
- [Agda] irrelevant fields and EqReasoning
Noam Zeilberger
- [Agda] irrelevant fields and EqReasoning
Jean-Philippe Bernardy
- [Agda] irrelevant fields and EqReasoning
Noam Zeilberger
- [Agda] beginner questions
Serge D. Mechveliani
- [Agda] beginner questions
Andreas Abel
- [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] Call for Papers: The 7th International Conference for
Internet Technology and Secured Transactions (ICITST-2012)!
y.zhao at icitst.org
- [Agda] Display of private things (for higher inductive types)
Andreas Abel
- [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] ICFP 2012: Second call for participation
Wouter Swierstra
- [Agda] ICFP 2012: Second call for participation
Wouter Swierstra
- [Agda] help with math symbols
Nils Anders Danielsson
- [Agda] beginner questions
Nils Anders Danielsson
- [Agda] Agda for CA
Nils Anders Danielsson
- [Agda] without-K problem
Nils Anders Danielsson
- [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
Serge D. Mechveliani
- [Agda] Bin._<_
Serge D. Mechveliani
- [Agda] Installing Agda
Jason Gross
- [Agda] help with math symbols
Dominique Devriese
- [Agda] Call for Participation: Implementation and Application of
Functional Languages 2012
Tom Harper
- [Agda] Bin._<_
James Deikun
- [Agda] help with math symbols
Guillaume Brunerie
- [Agda] Bin._<_
Nils Anders Danielsson
- [Agda] Bin._<_
James Deikun
- [Agda] help with math symbols
Serge D. Mechveliani
- [Agda] Bin._<_
Andreas Abel
- [Agda] Bin._<_
Serge D. Mechveliani
- [Agda] Installing Agda
Andreas Abel
- [Agda] TPNC 2012: 2nd call for posters
GRLMC
- [Agda] Bin._<_
James Deikun
- [Agda] GAMES 2012 -- Call for participation --
Nello Murano
- [Agda] Installing Agda
Jason Gross
- [Agda] irrelevant fields and EqReasoning
Nils Anders Danielsson
- [Agda] irrelevant fields and EqReasoning
Nils Anders Danielsson
- [Agda] help with math symbols
Nils Anders Danielsson
- [Agda] Bin._<_
Nils Anders Danielsson
- [Agda] Installing Agda
Nils Anders Danielsson
- [Agda] Building Agda with newer haskeline
Dirk Ullrich
- [Agda] help with math symbols
Serge D. Mechveliani
- [Agda] Installing Agda
Jason Gross
- [Agda] GandALF 2012 -- Call for participation --
Nello Murano
- [Agda] help with math symbols
Nils Anders Danielsson
- [Agda] equality on Integer
Serge D. Mechveliani
- [Agda] equality on Integer
Nils Anders Danielsson
- [Agda] Building Agda with newer haskeline
Nils Anders Danielsson
- [Agda] class inheritance
Serge D. Mechveliani
- [Agda] class inheritance
Nils Anders Danielsson
- [Agda] FSFLA 2012: 3rd announcement
GRLMC
- [Agda] Display of private things (for higher inductive types)
Guillaume Brunerie
- [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] CFP: Systems Software Verification (SSV'12)
Gerwin Klein
- [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] 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] on `data' syntax
Serge D. Mechveliani
- [Agda] Strictly positive types
Andrés Sicard-Ramírez
- [Agda] IEEE HLDVT 2012: Call for Work-in-Progress Abstracts
(Deadline: August 27, 2012)
Hiren D. Patel
- [Agda] on `data' syntax
Nils Anders Danielsson
- [Agda] Strictly positive types
Nils Anders Danielsson
- [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
- [Agda] Strictly positive types
Andrés Sicard-Ramírez
- [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] record with proof
Serge D. Mechveliani
- [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] `case' vs `with'
Serge D. Mechveliani
- [Agda] `case' vs `with'
Nils Anders Danielsson
- [Agda] Typed vs untyped lambda abstractions
Andreas Abel
- [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
- [yoshiki] [Agda] [REMINDER] Agda Intensive Meeting 16th (AIM XVI)
in Copenhagen
Rika T. Gotoh
- [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] ANN: Jekejeke Prolog 0.9.5 (runtime console, google play)
Jan Burse
- [Agda] _$_
Nils Anders Danielsson
- [Agda] Call for Lightning Talks / Challenges, Workshop on Generic
Programming 2012
Andres Löh
- [Agda] _divMod_
Serge D. Mechveliani
- [Agda] ANN: Jekejeke Prolog 0.9.5 (runtime console, google play)
Andreas Abel
- [Agda] _divMod_
Andreas Abel
- [Agda]
Re: ANN: Jekejeke Prolog 0.9.5 (runtime console, google play)
Jan Burse
- [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] 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] message of parameterized
Andreas Abel
- [Agda] message of parameterized
Serge D. Mechveliani
- [Agda] message of parameterized
Nils Anders Danielsson
- [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] Book Announcement
Gopalan Nadathur
- [Agda] congruence, Preserves_2
Serge D. Mechveliani
- [Agda] congruence, Preserves_2
Serge D. Mechveliani
- [Agda] Agdas constraint solver too eager?!
James Deikun
- [Agda] TPNC 2012: call for participation
GRLMC
- [Agda] Agdas constraint solver too eager?!
James Deikun
- [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] Agdas constraint solver too eager?!
Andreas Abel
- [Agda] Agdas constraint solver too eager?!
Andreas Abel
- [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] congruence, Preserves_2
Andreas Abel
- [Agda] congruence, Preserves_2
Andreas Abel
- [Agda] congruence, Preserves_2
Serge D. Mechveliani
- [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] Compiling Standard Library with GHC 7.6
Dirk Ullrich
- [Agda] monot-minus for Nat
Serge D. Mechveliani
- [Agda] monot-minus for Nat
Nils Anders Danielsson
- [Agda] divMod variant
Serge D. Mechveliani
- [Agda] FSNC 2012: 2nd announcement
GRLMC
- [Agda] Forget Hurken's Paradox,
Agda has a quicker route to success
Dan Doel
- [Agda] Compiling Standard Library with GHC 7.6
Lyndon Maydwell
- [Agda] Forget Hurken's Paradox, Agda has a quicker route to
success
Altenkirch Thorsten
- [Agda] LICS 2013 - Call for Papers
Andrzej Murawski
- [Agda] Forget Hurken's Paradox,
Agda has a quicker route to success
Andreas Abel
- [Agda] Compiling Standard Library with GHC 7.6
Andrés Sicard-Ramírez
- Phantom arguments [Re: [Agda] Agdas constraint solver too eager?!]
Andreas Abel
- [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] termination proofs
Serge D. Mechveliani
- [Agda] tuple patterns
Alan Jeffrey
- [Agda] termination proofs
gallais at ensl.org
- [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] Second Call for Papers: BEAT'13 - 1st International Workshop
on Behavioural Types
Hans Hüttel
- [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
Peter Hancock
- [Agda] termination proofs
Jacques Carette
- [Agda] termination proofs
Altenkirch Thorsten
- [Agda] termination proofs
Jacques Carette
- [Agda] `where' scope
Serge D. Mechveliani
- [Agda] termination proofs
Peter Hancock
- [Agda] termination proofs
Martin Escardo
- [Agda] termination proofs
Altenkirch Thorsten
- [Agda] Termination checking: valid or invalid
Wojciech Jedynak
- Compositional termination [Re: [Agda] Termination checking: valid
or invalid]
Andreas Abel
- [Agda] `where' scope
Andreas Abel
- [Agda] `where' scope
Serge D. Mechveliani
- [Agda] `where' scope
Serge D. Mechveliani
- [Agda] `where' scope
Nils Anders Danielsson
- [Agda] termination proofs
Serge D. Mechveliani
- [Agda] PEPM 2013: Final Call for Papers
Shin-Cheng Mu
- [Agda] termination proofs
Peter Hancock
- [Agda] termination proofs
Serge D. Mechveliani
- [Agda] termination proofs
Peter Hancock
- [Agda] Compositional termination
Karn Kallio
- [Agda] `where' scope
Cezar Ionescu
- [Agda] local needs override
Serge D. Mechveliani
- [Agda] termination proofs
Altenkirch Thorsten
- [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?
Nils Anders Danielsson
- [Agda] Does the order of patterns matter?
Martin Escardo
- [Agda] RTA 2013: First Call for Papers
Sophie Tison
- [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?
Andreas Abel
- [Agda] Does the order of patterns matter?
Altenkirch Thorsten
- [Agda] PEPM 2013: Deadline Extension
Shin-Cheng Mu
- [Agda] Does the order of patterns matter?
Andreas Abel
- [Agda] Does the order of patterns matter?
Martin Escardo
- [Agda] FSFLA 2012: final announcement
GRLMC
- [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] evaluation in compilation
Serge D. Mechveliani
- [Agda] evaluation in compilation
Nils Anders Danielsson
- [Agda] evaluation in compilation
Andreas Abel
- [Agda] PLPV 2013 Last Call for Papers
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
Nils Anders Danielsson
- [Agda] evaluation in compilation
Serge D. Mechveliani
- [Agda] evaluation in compilation
Serge D. Mechveliani
- [Agda] evaluation in compilation
Nils Anders Danielsson
- [Agda] readFile and output
Serge D. Mechveliani
- [Agda] Colist -> List
Serge D. Mechveliani
- [Agda] Colist -> List
Daniel Peebles
- [Agda] readFile and output
Serge D. Mechveliani
- [Agda] readFile and output
Nils Anders Danielsson
- [Agda] evaluation in compilation
Serge D. Mechveliani
- [Agda] Colist -> List
Andreas Abel
- [Agda] evaluation in compilation
Andreas Abel
- [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] 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] evaluation in compilation
Andreas Abel
- [Agda] evaluation in compilation
Serge D. Mechveliani
- [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] Date of AIM XVII fixed: 2013.5.8 - 5.14
KINOSHITA Yoshiki
- [Agda] syntax highlighting
Martin Escardo
- [Agda] @-patterns
Serge D. Mechveliani
- [Agda] @-patterns
Daniel Peebles
- [Agda] @-patterns
Daniel Peebles
- [Agda] @-patterns
Serge D. Mechveliani
- [Agda] syntax highlighting
Nils Anders Danielsson
- [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] FSNC 2012: 3rd announcement
GRLMC
- [Agda] proof run time cost
Andreas Abel
- [Agda] proof run time cost
Serge D. Mechveliani
- [Agda] direct product for list
Serge D. Mechveliani
- [Agda] direct product for list
Andreas Abel
- [Agda] direct product for list
Serge D. Mechveliani
- [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] `let' in record decl
Serge D. Mechveliani
- [Agda] direct product for list
Andreas Abel
- [Agda] `let' in record decl
Andreas Abel
- [Agda] `let' in record decl
Serge D. Mechveliani
- [Agda] direct product for list
Serge D. Mechveliani
- [Agda] Sharing --- Q-combinators
Wolfram Kahl
- [Agda] `let' in record decl
Serge D. Mechveliani
- [Agda] Sharing --- Q-combinators
Andreas Abel
- [Agda] `let' in record decl
Nicolas Pouillard
- [Agda] Total: x !<= y ==> y <= x
Serge D. Mechveliani
- [Agda] Sharing --- Q-combinators
wren ng thornton
- [Agda] Total: x !<= y ==> y <= x
wren ng thornton
- [Agda] Total: x !<= y ==> y <= x
Daniel Peebles
- [Agda] Sharing --- Q-combinators
Wolfram Kahl
- [Agda] Sharing --- Q-combinators
Peter Divianszky
- [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] Sharing --- Q-combinators
Andreas Abel
- [Agda] `let' in record decl
Andreas Abel
- [Agda] direct product for list
Andreas Abel
- [Agda] Sharing --- Q-combinators
Peter Divianszky
- [Agda] Sharing --- Q-combinators
Andreas Abel
- [Agda] `let' in record decl
Nils Anders Danielsson
- [Agda] `using (DecTotalOrder)'
Nils Anders Danielsson
- [Agda] Building Agda with ghc-6.12.3: build failure on geniplate
Nils Anders Danielsson
- [Agda] `let' in record decl
Andreas Abel
- [Agda] `let' in record decl
Nils Anders Danielsson
- [Agda] Building Agda with ghc-6.12.3: build failure on geniplate
Guillaume Brunerie
- [Agda] Indentation for abstract and private declarations
Guillaume Brunerie
- Let in telescopes, where to put the color? [Re: [Agda] `let' in record
decl]
Andreas Abel
- [Agda] Indentation for abstract and private declarations
Andreas Abel
- [Agda] Total: x !<= y ==> y <= x
Serge D. Mechveliani
- [Agda] Total: x !<= y ==> y <= x
Andrés Sicard-Ramírez
- [Agda] Indentation for abstract and private declarations
Wolfram Kahl
- [Agda] Sharing --- Q-combinators
Andreas Abel
- [Agda] Total: x !<= y ==> y <= x
Serge D. Mechveliani
- [Agda] Total: x !<= y ==> y <= x
Serge D. Mechveliani
- [Agda] `let' in record decl
Serge D. Mechveliani
- [Agda] `let' in record decl
Andreas Abel
- [Agda] `let' in record decl
Andreas Abel
- [Agda] Building Agda with ghc-6.12.3: build failure on geniplate
Dan Rosén
- [Agda] `let' in record decl
Nicolas Pouillard
- [Agda] unused bindings
Serge D. Mechveliani
- [Agda] Total: x !<= y ==> y <= x
Nils Anders Danielsson
- Let in telescopes, where to put the color? [Re: [Agda] `let'
in record decl]
Nils Anders Danielsson
- [Agda] moving common from `with'
Serge D. Mechveliani
- [Agda] Compiling Standard Library with GHC 7.6
Nils Anders Danielsson
- [Agda] Display of private things (for higher inductive types)
Nils Anders Danielsson
- [Agda] Compiling Standard Library with GHC 7.6
Lyndon Maydwell
- [Agda] moving common from `with'
Andreas Abel
- [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] Agda Unique type
Nils Anders Danielsson
- [Agda] Fairbairn not for St.lib
Serge D. Mechveliani
- [Agda] Fairbairn not for St.lib
Wolfram Kahl
- [Agda] moving common from `with'
Serge D. Mechveliani
- [Agda] Seg-fault
Serge D. Mechveliani
- [Agda] Agda Unique type
Dmytro Starosud
- [Agda] moving common from `with'
Andreas Abel
- [Agda] lists/vectors
Amr Sabry
- [Agda] LATA 2013: 3rd call for papers
GRLMC
- [Agda] moving common from `with'
Serge D. Mechveliani
- [Agda] moving common from `with'
Dan Doel
- [Agda] lists/vectors
Andrés Sicard-Ramírez
- [Agda] Seg-fault
Nils Anders Danielsson
- [Agda] `syntax'
Serge D. Mechveliani
- [Agda] lists/vectors
Nils Anders Danielsson
- [Agda] `syntax'
Nils Anders Danielsson
- [Agda] lists/vectors
Amr Sabry
- [Agda] lists/vectors (interfacing with untrusted code)
Amr Sabry
- [Agda] lists/vectors (interfacing with untrusted code)
gallais at ensl.org
- [Agda] lists/vectors
Amr Sabry
- [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
Dominique Devriese
- [Agda] Seg-fault
Wolfram Kahl
- [Agda] lists/vectors
Dominique Devriese
- [Agda] Seg-fault
Serge D. Mechveliani
- [Agda] Seg-fault
Serge D. Mechveliani
- [Agda] `syntax'
Serge D. Mechveliani
- [Agda] `syntax'
Daniel Peebles
- [Agda] moving common from `with'
Andreas Abel
- [Agda] parameterized modules?
Serge D. Mechveliani
- [Agda] `syntax'
Nils Anders Danielsson
- [Agda] moving common from `with'
Dan Doel
- [Agda] lists/vectors (interfacing with untrusted code)
Nils Anders Danielsson
- [Agda] lists/vectors
Nils Anders Danielsson
- [Agda] lists/vectors
Noam Zeilberger
- [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] parameterized modules?
Andreas Abel
- [Agda] Some module statements, for your amusement
Andreas Abel
- [Agda] parameterized modules?
Serge D. Mechveliani
- [Agda] laziness damaged
Serge D. Mechveliani
- [Agda] parameterized modules?
Andreas Abel
- [Agda] laziness damaged
Jeffrey, Alan S A (Alan)
- [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
- 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] laziness damaged
Serge D. Mechveliani
- [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] 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] DTO, STO, AVL.Tree
Serge D. Mechveliani
- [Agda] Agda pragmas are rendered incorrectly in lhs2tex
Andreas Abel
- [Agda] WSLST 2013: 1st announcement
GRLMC
- [Agda] Agda pragmas are rendered incorrectly in lhs2tex
Andrés Sicard-Ramírez
- [Agda] DTO, STO, AVL.Tree
Nils Anders Danielsson
- [Agda] DTO, STO, AVL.Tree
Serge D. Mechveliani
- [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
- 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
- [Agda] CFP: Term and Graph Rewriting (TERMGRAPH2013) / ETAPS2013
Wolfram Kahl
- Let in telescopes, where to put the color? [Re: [Agda] `let' in
record decl]
Nicolas Pouillard
- [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
- [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
- [Haskell-cafe] [Agda] How to avoid T3 fonts in pdf generated
with lhs2TeX?
Andreas Abel
- [Agda] Understanding productivity
Daniel Peebles
- [Agda] Understanding productivity
Andreas Abel
- [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] Understanding productivity
Nils Anders Danielsson
- [Agda] partial division property
Serge D. Mechveliani
- [Agda] partial division property
Serge D. Mechveliani
- [Agda] partial division property
Nils Anders Danielsson
- [Agda] windows installer is not available
Peter Divianszky
- [Agda] on "Dependently Typed.."
Serge D. Mechveliani
- [Agda] boundings in data-where
Serge D. Mechveliani
- [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] boundings in data-where
Serge D. Mechveliani
- Syntax of 'data' declaration [Re: [Agda] boundings in data-where]
Andreas Abel
- [Agda] on "Dependently Typed.."
Andreas Abel
- [Agda] skipped ambiguity?
Serge D. Mechveliani
- [Agda] on "Dependently Typed.."
James Chapman
- Syntax of 'data' declaration [Re: [Agda] boundings in data-where]
Serge D. Mechveliani
- [Agda] skipped ambiguity?
Andreas Abel
- Syntax of 'data' declaration [Re: [Agda] boundings in data-where]
Andreas Abel
- [Agda] data syntax ext.
Serge D. Mechveliani
- [Agda] Decidable _\~~_ of Semiring
Serge D. Mechveliani
- [Agda] Decidable _\~~_ of Semiring
Andreas Abel
- [Agda] SR 2013 - Call for contributions
Nello Murano
- [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] Decidable _\~~_ of Semiring
Daniel Peebles
- [Agda] Decidable _\~~_ of Semiring
Serge D. Mechveliani
- [Agda] `data'-record field overlap
Serge D. Mechveliani
- [Agda] Re: `data'-record field overlap
Francesco Mazzoli
- [Agda] `data'-record field overlap
Andreas Abel
- [Agda] Re: `data'-record field overlap
Francesco Mazzoli
- [Agda] CFP : 2nd International Workshop on Engineering Safety and
Security Systems (ESSS)
=?Big5?B?pHOnzr/gpKc=?=
- [Agda] Re: `data'-record field overlap
Andreas Abel
- [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
Andrés Sicard-Ramírez
- [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
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] Positivity check
Andrew Cave
- [Agda] Positivity check
Andreas Abel
- [Agda] Positivity check
Daniel Peebles
- [Agda] Unification assumes injective postulates?
Jan Malakhovski
- Fw: Re: [Agda] Unification assumes injective postulates?
Jan Malakhovski
- [Agda] Application for PhD Studentship
Kuttuvam Meeyakhan KhanMohamed
- [Agda] Problems with emacs agda-mode after upgrading to 2.3.2
Nils Anders Danielsson
- [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] Building utilities for Agda?
Darryl
- [Agda] Unification assumes injective postulates?
Andreas Abel
- [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] 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] Unification assumes injective postulates?
Jan Malakhovski
- [Agda] Unification assumes injective postulates?
Nils Anders Danielsson
- [Agda] Unification assumes injective postulates?
Jan Malakhovski
- [Agda] Question about the meaning of 'abstract'
Dan Licata
- [Agda] with + continuation
Peter Divianszky
- [Agda] Re: with + continuation
Peter Divianszky
- [Agda] Re: with + continuation
Andreas Abel
- [Agda] Two papers on Agda and FRP
Andreas Abel
- [Agda] Re: with + continuation
Peter Divianszky
- [Agda] Call for Participation: Programming Languages Mentoring
Workshop - a POPL workshop.
Gareth Smith
- [Agda] Re: with + continuation
Peter Divianszky
- [Agda] Question about the meaning of 'abstract'
Andreas Abel
- [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] optional dot in dot patterns?
Peter Divianszky
- [Agda] function parameters similar to data parameters
Dominique Devriese
- [Agda] Question about the meaning of 'abstract'
Nils Anders Danielsson
- [Agda] optional dot in dot patterns?
Nils Anders Danielsson
- [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] optional dot in dot patterns?
Nils Anders Danielsson
- [Agda] Classical Mathematics for a Constructive World
Martin Escardo
- [Agda] optional dot in dot patterns?
Peter Divianszky
- [Agda] Re: Classical Mathematics for a Constructive World
Jan Burse
- [Agda] optional dot in dot patterns?
Dan Doel
- [Agda] Re: with + continuation
Twan van Laarhoven
- [Agda] optional dot in dot patterns?
Peter Divianszky
- vertical application (Re: [Agda] Re: with + continuation)
Peter Divianszky
- [Agda] optional dot in dot patterns?
Andreas Abel
- [Agda] Re: Classical Mathematics for a Constructive World
Jan Burse
- [Agda] Re: Classical Mathematics for a Constructive World
Martin Escardo
- [Agda] optional dot in dot patterns?
Peter Divianszky
- [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] Re: Agda Digest, Vol 87, Issue 24
Valeria de Paiva
- [Agda] Re: Agda Digest, Vol 87, Issue 24
Martin Escardo
- [Agda] ITP 2013: Call for workshop proposals
David Pichardie
- [Agda] Unification assumes injective postulates?
Nils Anders Danielsson
- [Agda] function parameters similar to data parameters
Andreas Abel
- [Agda] function parameters similar to data parameters
Andreas Abel
- [Agda] Data.Setoid ?
Jacques Carette
- [Agda] Positivity check
Andrew Cave
- [Agda] Data.Setoid ?
Wolfram Kahl
- [Agda] function parameters similar to data parameters
Peter Divianszky
- [Agda] agsy extensions
Peter Divianszky
- [Agda] StdLib additions
Peter Divianszky
- [Agda] Re: Agda Digest, Vol 87, Issue 24
Dan Licata
- [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] StdLib additions
Daniel Peebles
- [Agda] DICE 2013, second call for papers
Simona Ronchi della Rocca
- [Agda] Classical Mathematics for a Constructive World
Peter Divianszky
- [Agda] function parameters similar to data parameters
Andreas Abel
- [Agda] agsy extensions
Andreas Abel
- [Agda] Classical Mathematics for a Constructive World
Martin Escardo
- [Agda] Classical Mathematics for a Constructive World
Peter Divianszky
- [Agda] function parameters similar to data parameters
Peter Divianszky
- [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
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
Martin Escardo
- [Agda] Classical Mathematics for a Constructive World
wren ng thornton
- [Agda] Classical Mathematics for a Constructive World
Peter Hancock
- [Agda] function parameters similar to data parameters
Nils Anders Danielsson
- [Agda] StdLib additions
Nils Anders Danielsson
- [Agda] Classical Mathematics for a Constructive World
Peter Divianszky
- [Agda] Re: Agda Digest, Vol 87, Issue 24
Altenkirch Thorsten
- [Agda] ITP 2013: First Call for Papers
David Pichardie
- [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] 10th Annual Conference on Theory and Applications of Models
of Computation (TAMC13)
S B Cooper
- [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
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
Dan Licata
- [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
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
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] : vs. ∶
Nils Anders Danielsson
- [Agda] Classical Mathematics for a Constructive World
Martin Escardo
- [Agda] : vs. ∶
Wolfram Kahl
- [Agda] : vs. ∶
Andreas Abel
- [Agda] TLCA 2013 Second Call for Papers
Luca Paolini
- [Agda] : vs. ∶
Nils Anders Danielsson
- [Agda] : vs. ∶
Nils Anders Danielsson
- [Agda] : vs. ∶
Cezar Ionescu
- Re: [Agda] : vs. ∶
Dominique Devriese
- [Agda] : vs. ∶
Wolfram Kahl
- [Agda] : vs. ∶
Alan Jeffrey
- [Agda] : vs. ∶
Wolfgang Jeltsch
- [Agda] : vs. ∶
Wolfgang Jeltsch
- [Agda] : vs. ∶
Wolfgang Jeltsch
- Re: [Agda] : vs. ∶
Jean-Philippe Bernardy
- [Agda] : vs. ∶
Nils Anders Danielsson
- [Agda] CiE 2013: The Nature of Computation, Milan, Italy, July 1-5,
2013
S B Cooper
- Re: [Agda] : vs. ∶
Darryl
- [Agda] algebra libraries
Serge D. Mechveliani
- [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] algebra libraries
Nils Anders Danielsson
- [Agda] : vs. ∶
Nils Anders Danielsson
- Re: [Agda] : vs. :
Altenkirch Thorsten
- [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] goal normalization request
Darryl
- [Agda] goal normalization request
Andreas Abel
- [Agda] PEPM 2013: 2nd Call for Participation
Shin-Cheng Mu
- [Agda] goal normalization request
Nils Anders Danielsson
- [Agda] goal normalization request
Darryl
- [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
- [Agda] Patch to build with `hashable-1.2.x'
Dirk Ullrich
- [Agda] Special issue of MSCS: extended deadline
Nicola Gambino
- [Agda] Re: Agda Digest, Vol 87, Issue 24
Dan Licata
- [Agda] SR 2013 - Extended Deadline and Last Call for Contributions
Nello Murano
- Linear Pattern Inductive Famlies [Re: [Agda] no longer type
checks]
Andreas Abel
- [Agda] Classical Mathematics for a Constructive World
Peter Divianszky
- [Agda] Classical Mathematics for a Constructive World
Andreas Abel
- [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] Re: Classical Mathematics for a Constructive World
Jan Burse
- [Agda] no longer type checks
Nils Anders Danielsson
- [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] no longer type checks
Andreas Abel
- [Agda] CSL 2013 : PRELIMINARY ANNOUNCEMENT
Luca Paolini
- [Agda] no longer type checks
Nils Anders Danielsson
- [Agda] Patch to build with `hashable-1.2.x'
Nils Anders Danielsson
- [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] Highest Level seen?
Jacques Carette
- [Agda] Re: ghc for Agda-2.3.2
Francesco Mazzoli
- [Agda] Highest Level seen?
Dan Doel
- [Agda] Semigroup.Carrier in 2.3.2
Serge D. Mechveliani
- [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] Highest Level seen?
Darryl
- [Agda] Highest Level seen?
Jacques Carette
- [Agda] Highest Level seen?
Darryl
- [Agda] ghc for Agda-2.3.2
Andreas Abel
- [Agda] Semigroup.Carrier in 2.3.2
Andreas Abel
- [Agda] ESSS 2013 -- submission deadline extended
=?Big5?B?pHOnzr/gpKc=?=
- [Agda] list member error
Serge D. Mechveliani
- [Agda] Patch to build with `hashable-1.2.x'
Dirk Ullrich
- [Agda] Highest Level seen?
Nils Anders Danielsson
- [Agda] list member error
Andreas Abel
- [Agda] Semigroup.Carrier in 2.3.2
Andreas Abel
- 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] Semigroup.Carrier in 2.3.2
Serge D. Mechveliani
- [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
This archive was generated by
Pipermail 0.09 (Mailman edition).