2015 Archives by thread
Starting: Thu Jan 1 18:57:31 CEST 2015
Ending: Thu Dec 31 20:03:18 CEST 2015
Messages: 1034
- [Agda] enigmatic `with'
Sergei Meshveliani
- [Agda] simple question
Andrew Harris
- [Agda] struggling `with'
Sergei Meshveliani
- [Agda] Re: How can I prove associativity of vectors?
Helmut Grohne
- [Agda] Inspect.
Andrés Sicard-Ramírez
- [Agda] new use for literate agda!
Thorsten Altenkirch
- [Agda] ... n ∸ m > 0
Sergei Meshveliani
- [Agda] TYPES 2015 call for contributions
Tarmo Uustalu
- [Agda] Mathematics of Program Construction (MPC 2015): final call
for papers
José Pedro Magalhães
- [Agda] Termination checking (perhaps could be smarter)
Carlos Camarao
- [Agda] Univalence via Agda's primTrustMe?
Alan Jeffrey
- [Agda] Agda master is anti-classical,
injective type constructors are back
Andreas Abel
- [Agda] Set properties
Carlos Camarao
- [Agda] Re: Issue 1402 in agda: Where clauses in rewrite RHS cause
internal error
Sergei Meshveliani
- [Agda] Set properties
Carlos Camarao
- [Agda] printed goal type
Sergei Meshveliani
- [Agda] `Respects'
Sergei Meshveliani
- [HoTT] Re: [Agda] Univalence via Agda's primTrustMe?
Alan Jeffrey
- [Agda] Univalence via Agda's primTrustMe again
Alan Jeffrey
- [Agda] Mutual data definitions
Dominique Devriese
- [Agda] post-doc and visiting positions at wesleyan
Dan Licata
- [Agda] PhD positions in Utrecht
Wouter Swierstra
- [Agda] Agda Tutorial darcs repo & pandoc backend
Peter Divianszky
- [Agda] First Call for Papers, PxTP 2015
Andrei Paskevich
- [Agda] A new rewrite 'tactic'.
Victor Miraldo
- [Agda] question on `compare'
Sergei Meshveliani
- [Agda] Wrong reporting error ? (Was question on `compare')
Andrés Sicard-Ramírez
- [Agda] Inheriting fields
N. Raghavendra
- [Agda] Poll: Remove the Agda interactive mode
Andrés Sicard-Ramírez
- [Agda] Indentation in stdlib files
N. Raghavendra
- [Agda] [TFP 2015] 2nd call for papers
Peter Achten
- [Agda] ICFP 2015: Final Call for Papers
David Van Horn
- [Agda] TYPES 2015 2nd call for contributions
Tarmo Uustalu
- [Agda] How to define subsemigroups
N. Raghavendra
- [Agda] pointwise congr.of ++
Sergei Meshveliani
- [Agda] Journal of Formalized Reasoning opens a section for PhD/HDR
thesis
Enrico Tassi
- [Agda] Forall and product
N. Raghavendra
- [Agda] Univalence via Agda's primTrustMe again^2
Alan Jeffrey
- [Agda] Fin n -> Fin n extensional?
Jacques Carette
- [Agda] AIM XIX 3-9 June 2015: Save the date!
Andreas Abel
- [Agda] Irrationality proof
N. Raghavendra
- [Agda] A HoTT-Date with Thorsten Altenkirch at Strathclyde 04.03.15
Fredrik Nordvall Forsberg
- [Agda] Strictly positive
Kenichi Asai
- [Agda] ANN: PandocAgda 2.4.3
Peter Divianszky
- [Agda] How to install Epic for Agda?
Jesper Cockx
- [Agda] CfP: UF/HoTT workshop, Warsaw, 29--30 June, with TLCA 2015
Peter LeFanu Lumsdaine
- [Agda] Midlands Graduate School 2015
Thorsten Altenkirch
- [Agda]
PhD student, dependent types/functional programming, Chalmers
Nils Anders Danielsson
- [Agda] PhD position in dependent types/functional programming at
Chalmers
Andreas Abel
- [Agda] PhD position in dependent types/functional programming at
Chalmers
Andreas Abel
- [Agda] PhD position in dependent types/functional programming at
Chalmers
Andreas Abel
- [Agda] AlCoB 2015: extended submission deadline 9 March
GRLMC
- [Agda] DSLDI: 3rd Workshop on Domain-Specific Language Design and
Implementation
Tijs van der Storm
- [Agda] [TFPIE 2015] 2nd call for papers
Peter Achten
- [Agda] --termination-depth
Sergei Meshveliani
- [Agda] CFP: Workshop on Generic Programming 2015 - Deadline May 15
Sebastian Erdweg
- [Agda] Data.Nat.Primality.Prime and irreducibility
N. Raghavendra
- [Agda] primality definition
Sergei Meshveliani
- [Agda] Accessing fields of algebra records
N. Raghavendra
- [Agda] Re: Accessing fields of algebra records
Sergei Meshveliani
- [Agda]
Defining large numbers without recursion, with short programs
Martin Escardo
- [Agda] HoTT-Agda question
Jacques Carette
- [Agda] Help, I'm failing at sized types.
Conor McBride
- [Agda] unused values
Sergei Meshveliani
- [Agda] TYPES 2015 submission deadline extended
Tarmo Uustalu
- [Agda] Decidable _\equiv_
Sergei Meshveliani
- [Agda] [TFP'15] final call for papers - extended deadline march 31 -
Peter Achten
- [Agda] CFP: ACM SIGPLAN GPCE 2015
Faruk Caglar
- [Agda] +-mono arguments
Sergei Meshveliani
- [Agda] fast DecTotalOrder
Sergei Meshveliani
- [Agda] Mentoring workshop @ ICFP
Stephanie Weirich
- [Agda] type check performance
Sergei Meshveliani
- [Agda] Poll: Remove the Epic back-end
Andrés Sicard-Ramírez
- [Agda] DSLDI: 3rd Workshop on Domain-Specific Language Design and
Implementation (EXTENDED DEADLINE)
Tijs van der Storm
- [Agda] A problem with instance arguments and function application.
effectfully
- [Agda] Agda 2.4.2.2: Bumped upper version bound for hashtables
Andrés Sicard-Ramírez
- [Agda] Agda beginner.
Serge Leblanc
- [Agda] Lit Agda and MMM mode
N. Raghavendra
- [Agda] URLs in comments
N. Raghavendra
- [Agda] HoTT/UF workshop at TLCA Warsaw: abstract deadline Apr 15
Peter LeFanu Lumsdaine
- [Agda] DoCon-A announcement
Sergei Meshveliani
- [Agda] Positive but not strictly positive types
Andrés Sicard-Ramírez
- [Agda] Last Call for Papers, PxTP 2015
Andrei Paskevich
- [Agda] Positive but not strictly positive types
Thorsten Altenkirch
- [Agda] Positive but not strictly positive types
Thorsten Altenkirch
- [Agda] Implicit arguments
N. Raghavendra
- [Agda] a puzzle about pattern matching
Aaron Stump
- [Agda] Strathclyde PhD Position
Conor McBride
- [Agda] AI4FM 2015: Call for Short Contributions
Iain Whiteside
- [Agda] record field as Instance Argument
Guillermo Calderon - INCO
- [Agda] Type-preserving renaming and substitutions for a dependently
typed lambda calculus.
effectfully
- [Agda] Builtins
N. Raghavendra
- [Agda] DoCon-A link
Sergei Meshveliani
- [Agda] Sane whitespace with agda --latex
Mateusz Kowalczyk
- [Agda] Final CFP: Workshop on Generic Programming 2015 - Deadline
May 15
Sebastian Erdweg
- [Agda] Agda meeting 3-9 June in Gothenburg, call for participation
Andrea Vezzosi
- [Agda] FLOPS 2016 CFP
Andreas Abel
- [Agda] LFMTP abstracts due 1st May
Andreas Abel
- [Agda] How can we define a type of symmetric binary operations in
Agda ?
Sergey Kirgizov
- [Agda] Using .Xcompose file on Fedora 21
Colin Adams
- [Agda] [TFP'15] call for participation
Peter Achten
- [Agda] Absurd patterns inconsistent with function extensionality
Gabe Dijkstra
- [Agda] TYPES 2015 call for participation
Tarmo Uustalu
- [Agda] Can't build index.html in HoTT-Agda repository
Colin Adams
- [Agda] Can't build index.html in HoTT-Agda repository
Andreas Abel
- [Agda] FICS'15 Call for papers - Fixed Points in Computer Science
(CSL'15 workshop 11+12 sept. 2015)
Ralph Matthes
- [Agda] Summer School on Generic and Effectful Programming
Maciej Pirog
- [Agda] PhD studentship in Nottingham available
Thorsten Altenkirch
- [Agda] First Call for Papers for IFL 2015
publicityifl at gmail.com
- [Agda] ANNOUNCE: Agda 2.4.2.2
Byron Hale
- [Agda] documents on the implementation of agda2-mode?
Kenichi Asai
- [Agda] Quotient types in Agda, if you Trust Me
Andrew Pitts
- [Agda] Deadline extension: Workshop on Generic Programming 2015 -
New deadline May 22
Sebastian Erdweg
- [Agda] literate colours
Martin Escardo
- [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate
Andrés Sicard-Ramírez
- [Agda] ANNOUNCE: Agda 2.4.2.3 release
Andrés Sicard-Ramírez
- [Agda] Deadline Approaching - CFP: ACM SIGPLAN GPCE 2015
Faruk Caglar
- [Agda] open import public
Andrew Pitts
- [Agda] instance argument problems
Andrew Pitts
- [Agda] Parameterized modules
Bruno Bianchi
- [Agda] Type a = Set a
Sergei Meshveliani
- [Agda] Type a = Set a
Alexander Altman
- [Agda] Strange behaviour of instance search.
effectfully
- [Agda] Re: Type a = Set a
Sergei Meshveliani
- [Agda] Sized Natural Numbers
Bruno Bianchi
- [Agda] agda slow
Thorsten Altenkirch
- [Agda] Agda dies trying to prove transitivity
Peter Thiemann
- [Agda] profiling
Sergei Meshveliani
- [Agda] Associativity and Heterogeneous Equality
Marco Vassena
- [Agda] FICS'15: 2nd call for papers - Fixed Points in Computer
Science (CSL'15 workshop 11+12 sept. 2015)
Ralph Matthes
- [Agda] on parametric modules
Sergei Meshveliani
- [Agda] generic map-cong
Sergei Meshveliani
- [Agda] Reflection and Application terms
Philipp Hausmann
- [Agda] AIM XXII: proposed date
Jesper Cockx
- [Agda] mutual recursion on vectors?
Kenichi Asai
- [Agda] ICFP 2015 Student Research Competition: Final Call for
Submissions
Andrew Kennedy
- [Agda] Agda meeting 16-22 September in Leuven,
call for participation
Jesper Cockx
- [Agda] Deadline Extension: ICFP 2015 Student Research Competition
Andrew Kennedy
- [Agda] symbol for a singleton set
Sergei Meshveliani
- [Agda] "Not a valid let-declaration"
Sergei Meshveliani
- [Agda] arguments in `data' pattern
Sergei Meshveliani
- [Agda] Should not _ patterns be resolvable by inaccessible patterns?
Andreas Abel
- [Agda] segmentation fault
Sergei Meshveliani
- [Agda] Agda can't find an obvious instance.
effectfully
- [Agda] HOTT-style reals in Agda
Joachim Breitner
- [Agda] question about a form of irrelevance elimination
Andrew Pitts
- [Agda] ICFP 2015 Call for Participation
David Van Horn
- [Agda] where definitions and with
Guillermo Calderon
- [Agda] Overloading atoms and operators
Andreas Abel
- [Agda] installing agda-2.4.2.3
Sergei Meshveliani
- [Agda] next year memberships at the IAS
Vladimir Voevodsky
- [Agda] Renaming of a module, associated with a record,
doesn't hide the original name.
effectfully
- [Agda] Renaming of a module, associated with a record, doesn't
hide the original name.
Andreas Abel
- [Agda] Renaming of a module, associated with a record, doesn't
hide the original name.
effectfully
- [Agda] Renaming of a module, associated with a record, doesn't
hide the original name.
Andreas Abel
- [Agda] Renaming of a module, associated with a record, doesn't
hide the original name.
effectfully
- [Agda] Renaming of a module, associated with a record, doesn't
hide the original name.
Andreas Abel
- [Agda] Renaming of a module, associated with a record, doesn't
hide the original name.
effectfully
- [Agda] Renaming of a module, associated with a record, doesn't
hide the original name.
Nicolas Pouillard
- [Agda] Renaming of a module, associated with a record, doesn't
hide the original name.
Andreas Abel
- [Agda] Renaming of a module, associated with a record, doesn't
hide the original name.
Nicolas Pouillard
- [Agda] An Agda proof of the Church-Rosser theorem
roconnor at theorem.ca
- [Agda] Universe-Heterogeneous tree
Philipp Hausmann
- [Agda] Stop creating or modifying issues in Google Code
Andrés Sicard-Ramírez
- [Agda] New bug tracker for Agda
Andrés Sicard-Ramírez
- [Agda] Explain this strange effect from the order of arguments (and
provide a workaround, if possible)
Martin Stone Davis
- [Agda] tweaking evaluation
Peter Selinger
- [Agda] type check performance
Sergei Meshveliani
- [Agda] change in operator syntax
Sergei Meshveliani
- [Agda] The proving cycle.
effectfully
- [Agda] A sticky refusal
Martin Stone Davis
- [Agda] type check cost for `open'
Sergei Meshveliani
- [Agda] Reminder: AIM XXII is in one month!
Jesper Cockx
- [Agda] Internship Opportunity at Galois: Winter/Sprint 2016
Ryan Wright
- [Agda] CFP: 25th International Conference on Compiler Construction
(CC)
Manuel Hermenegildo
- [Agda] simple with->case fail
mechvel at scico.botik.ru
- [Agda] Perplexed in a proof
Martin Stone Davis
- [Agda] FLOPS 2016 last cfp (deadline 21st Sep)
Andreas Abel
- [Agda] Post-doctoral position in interactive theorem proving at the
University of Iowa
Chantal Keller
- [Agda] Lambda terms as a natural transformation.
effectfully
- [Agda] Bundlling Agda with agda-writer
Andrej Bauer
- [Agda] Last few remarks before AIM XXII
Jesper Cockx
- [Agda] ANNOUNCE: Agda 2.4.2.4 release candidate
Andrés Sicard-Ramírez
- [Agda] TYPES 2015 post-proceedings open call for papers
Tarmo Uustalu
- [Agda] agdai size
Sergei Meshveliani
- [Agda] unused values
Sergei Meshveliani
- [Agda] Agda Questions.
Ismail Alyassiri
- [Agda] Performance issues with --sharing
Peter Selinger
- [Agda] [ANNOUNCE] Standard library 0.10
Andrés Sicard-Ramírez
- [Agda] modules named `_`
David Darais
- [Agda] [ANNOUNCE] Agda 2.4.2.4
Andrés Sicard-Ramírez
- [Agda] Permanent position at the University of Sussex
Martin Berger
- [Agda] Reminder: CPP deadline is coming up!
Dan Licata
- [Agda] TYPES 2015 post-proceedings open call for papers (reminder)
Tarmo Uustalu
- [Agda] --sharing
Sergei Meshveliani
- [Agda] type check cost
mechvel at scico.botik.ru
- [Agda] `abstract' fail
mechvel at scico.botik.ru
- [Agda] CFP: Special issue of JFP on dependently typed programming
Wouter Swierstra
- [Agda] Where did "agda2 include dirs" go?
Jesper Cockx
- [Agda] using `abstract'
Sergei Meshveliani
- [Agda] Polymorphism is not (always) naturality
Andrea Vezzosi
- [Agda] Heterogeneous equality of pairs and records: some questions.
Matteo Acerbi
- [Agda] type annotation in-place
Sergei Meshveliani
- [Agda] -1 as identifier
Sergei Meshveliani
- [Agda] Error defining Universe Polymorphism
Ashish Mishra
- [Agda] type check cost
Sergei Meshveliani
- [Agda] 2016-2017 at the IAS
Vladimir Voevodsky
- [Agda] HO logic
Sergei Meshveliani
- [Agda] Agda under emacs
Sergei Meshveliani
- [Agda] Inconsistent rewrite behavior
Martin Stone Davis
- [Agda] Strathclyde Chancellor’s Fellowship research positions (5 years)
Fredrik Nordvall Forsberg
- [Agda] PhD and Postdoc Positions - KWARC, Jacobs University Bremen
Michael Kohlhase
- [Agda] Releasing app with bundled Agda
Marko Koležnik
- [Agda] How to typecheck "How to keep your Neighbours in Order" in
the latest version of Agda
Martin Stone Davis
- [Agda] ICFP 2016 Call for Workshop and Co-located Event Proposals
Lindsey Kuper
- [Agda] Coinductive types and 'duals' to dependent lambda calculus?
Lars Lindqvist
- [Agda] Coinductive types and 'duals' to dependent lambda calculus?
Lars Lindqvist
- [Agda] Type Checking in Agda
Ashish Mishra
- [Agda] Coinductive types and 'duals' to dependent lambda calculus?
Lars Lindqvist
- [Agda] Coinductive types and 'duals' to dependent lambda calculus?
Thorsten Altenkirch
- [Agda] [ANNOUNCE] Standard library 0.11
Andrés Sicard-Ramírez
- [Agda] Komencenta demando.
Serge Leblanc
- [Agda] Agda documentation
Ulf Norell
- [Agda] Type Mismatch in with
Ashish Mishra
- [Agda] Agda Writer - a GUI for Agda on OS X
Andrej Bauer
- [Agda] operator treating
Sergei Meshveliani
- [Agda] Understanding Agda error messages
Martin Stone Davis
- [Agda] Reasoning with Pattern Match with Default Cases
Marco Vassena
- [Agda] More aggressive `with`: Please check your Agda-2.4.2
developments!
Andreas Abel
- [Agda] Komencenta demando.
Serge Leblanc
- [Agda] More aggressive `with`: Please check your Agda-2.4.2
developments!
darais at cs.umd.edu
- [Agda] SIGPLAN John C Reynolds Doctoral Dissertation Award
Jeremy Gibbons
- [Agda] trouble with let and where
Peter Selinger
- [Agda] PhD studentships at the Functional Programming Lab in
Nottingham
Thorsten Altenkirch
- [Agda] JFP Issue on Dependently typed programming: second call for
papers
Wouter Swierstra
- [Agda] (All P) Respects =pointwise
Sergei Meshveliani
- [Agda] ICFP 2016 Call for Papers
Lindsey Kuper
- [Agda] NASA Formal Methods 2016
MUNOZ, CESAR (LARC-D320)
- [Agda] how to run and test the basic function in agda
Mandy Martino
- [Agda] MSFP 2016: Call for Papers
Bob Atkey
- [Agda] 2016 Heidelberg Laureates Forum
Vladimir Voevodsky
- [Agda] FYI: Rationals in Idris
Andreas Abel
- [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate
Andrés Sicard-Ramírez
- [Agda] More heterogeneous equality.
effectfully
- [Agda] how to use monoid solver and how to derive a concept monoid
if assume we do not know monoid
Mandy Martino
- [Agda] PhD scholarship on foundations of meta-programming
Martin Berger
- [Agda] My MSc Dissertation
Ali Onaissi
- [Agda] ITP 2016: Call for papers
Nils Anders Danielsson
- [Agda] [ANNOUNCE] Agda 2.4.2.5
Andrés Sicard-Ramírez
- [Agda] how to run helloworld in agda
Mandy Martino
- [Agda] testing unifier
Sergei Meshveliani
- [Agda] Is it possible to switch off universes checking?
effectfully
- [Agda] Why no impredicative prop?
Timothy Carstens
- [Agda] command line type checker vs interactive
Sergei Meshveliani
Last message date:
Thu Dec 31 20:03:18 CEST 2015
Archived on: Thu Dec 31 20:05:54 CEST 2015
This archive was generated by
Pipermail 0.09 (Mailman edition).