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