2017 Archives by thread
Starting: Wed Jan 4 21:58:07 CET 2017
Ending: Sun Dec 31 17:07:28 CET 2017
Messages: 734
- [Agda] [newbie] universe levels and BUILTIN EQUALITY
Martin Stone Davis
- [Agda] [ANNOUNCE] Agda 2.5.2
Kenichi Asai
- [Agda] <Programming> 2017: Call for workshop, symposium & poster submissions
Tim Molderez
- [Agda] type check performance
Sergei Meshveliani
- [Agda] 'finitely supported' constructively and without decidable equality
Nils Anders Danielsson
- [Agda] I am failing at Sized types 2.
Apostolis Xekoukoulotakis
- [Agda] strictness switch
Sergei Meshveliani
- [Agda] <Programming> 2017: Final call for workshop, symposium, demo & poster submissions
Tim Molderez
- [Agda] TYPES 2017 call for contributions
Ambrus Kaposi
- [Agda] hidden agda options / getting more info about unsolved metas
Martin Stone Davis
- [Agda] pattern for All is not matched
Sergei Meshveliani
- [Agda] strange let-in-case-let
Sergei Meshveliani
- [Agda] Holes 0.1.0
Bradley Hardy
- [Agda] Multiple Research Positions, ERC MATHADOR Project, IMDEA Software Institute, Madrid, Spain
Germán Andrés Delbianco
- [Agda] Levels and Containers
Manuel Bärenz
- [Agda] Removing a deducible Size constrain leads to error.
Apostolis Xekoukoulotakis
- [Agda] `case' vs `with'
Sergei Meshveliani
- [Agda] Second Call for Papers: ICFP 2017
Lindsey Kuper
- [Agda] WiL 2017: Women in Logic Workshop Second Call for Papers (new dates)
Amy Felty
- [Agda] example with insertion to list
Sergei Meshveliani
- [Agda] ARCADE Call for Papers
Dmitriy Traytel
- [Agda] Math Research Communities on Homotopy Type Theory, June 4-10, 2017, Snowbird UT
Dan Licata
- [Agda] [Coq-Club] ESSLLI student session CFP: Deadline extended until Feb 14
Andreas Abel
- [Agda] Agda installation for all users
Kenichi Asai
- [Agda] 1st CfP: SLE 2017 (10th ACM SIGPLAN International Conference on Software Language Engineering)
Andrei Chis
- [Agda] Sized types unification error.
Apostolis Xekoukoulotakis
- [Agda] Fully funded PhD position in CS at Heriot-Watt University, Edinburgh, Scotland
Ekaterina Komendantskaya
- [Agda] Failed to find source of module
Sergei Meshveliani
- [Agda] proof for insertion to a list
Sergei Meshveliani
- [Agda] Proofs about programs explicitly represented in Agda.
K V S Prasad
- [Agda] text-icu-0.7.0.1
Sergei Meshveliani
- [Agda] {} for nested `with' syntax
Sergei Meshveliani
- [Agda] 1st call for papers: Trends in Functional Programming, 19-21 june 2017, University of Kent, Canterbury
Peter Achten
- [Agda] LOLA 2017: Call for Talk Proposals
Noam Zeilberger
- [Agda] Oregon PL Summer School 2017: call for participation
Amal Ahmed
- [Agda] Final Call for Papers: ICFP 2017
Lindsey Kuper
- [Agda] VSTTE 2017 - First Call for Papers
Andrei Paskevich
- [Agda] CALL FOR PAPERS - GraMSec 2017
Harley D. Eades III
- [Agda] more about insertion to a list
Sergei Meshveliani
- [Agda] AMMCS-2017 call for submissions
Jacques Carette
- [Agda] TYPES 2017 2nd call for contributions
Ambrus Kaposi
- [Agda] FYI: CFP CICM 2017
Patrik Jansson
- [Agda] AIM XXV - Gothenburg, May 9 - 15
Víctor López Juan
- [Agda] Call for participation: Workshop on Computer-aided Mathematical Proof, Cambridge UK, 10-14 July 2017
Andrew Pitts
- [Agda] Propositional equality for coinductive records
Jannis Limperg
- [Agda] signature for `with' branch
Sergei Meshveliani
- [Agda] example with nested `with'
Sergei Meshveliani
- [Agda] Using machine integers / Data.Int from Haskell in Agda
stvienna wiener
- [Agda] Adding "print" to TC monad?
Jon Sterling
- [Agda] FOREIGN GHC pragma triggers parse error
Shin-Cheng Mu
- [Agda] How safe is Type:Type?
Andreas Abel
- [Agda] <Programming> 2017: Call for participation
Tim Molderez
- [Agda] TYPES 2017 submission deadline extended
Ambrus Kaposi
- [Agda] productivity of fibonacci stream
Noam Zeilberger
- [Agda] Fix emacs compile hook after updating to new agda version
stvienna wiener
- [Agda] Two PhD positions in Ljubljana starting October 2017
Andrej Bauer
- [Agda] Maintain compatibility with ghc 7.8?
Andreas Abel
- [Agda] Oregon PL Summer School 2017: register by April 1
Amal Ahmed
- [Agda] Trouble with sizes
Manuel Bärenz
- [Agda] Agda options
Sergei Meshveliani
- [Agda] Call for Contributions: Foundations for Practical Formalization of Mathematics
Benedikt Ahrens
- [Agda] Date for PhD defense
Martin Escardo
- [Agda] First call for talk proposals: Higher-Order Programming with Effects, HOPE 2017
François Pottier
- [Agda] Many ways to open a module - Is there a reason?
Apostolis Xekoukoulotakis
- [Agda] about serialization
Sergei Meshveliani
- [Agda] PPDP 2017: Call For Papers
Brigitte Pientka
- [Agda] the Racket summer school of semantics and languages
Robby Findler
- [Agda] help explaining instance resolution
Martin Stone Davis
- [Agda] pattern matching order
Thorsten Altenkirch
- [Agda] CFP: Workshop on Type-driven Development (TyDe '17)
Brent Yorgey
- [Agda] 2nd call for papers: Trends in Functional Programming, 19-21 june 2017, University of Kent, Canterbury
Peter Achten
- [Agda] OPLSS: register by April 15th
Amal Ahmed
- [Agda] Autumn school "Proof and Computation"
Chuangjie Xu
- [Agda] Case split creates too many {_}
Apostolis Xekoukoulotakis
- [Agda] Vezzosi's patch
Sergei Meshveliani
- [Agda] making a pair explodes
Sergei Meshveliani
- [Agda] Typing.CheckRHS
Sergei Meshveliani
- [Agda] old .agdai
Sergei Meshveliani
- [Agda] VSTTE 2017 - Second Call for Papers
Andrei Paskevich
- [Agda] length-* in library
Sergei Meshveliani
- [Agda] ⊓ in Nat
Sergei Meshveliani
- [Agda] 6 Assistant professor positions at the University of Utrecht
Wouter Swierstra
- [Agda] VSTTE 2017 - Deadline Extension
Andrei Paskevich
- [Agda] Senior Lectureships in Computer Science at Chalmers and Gothenburg U
Andreas Abel
- [Agda] Problems with strict positivity
Manuel Bärenz
- [Agda] Call for participation: TYPES 2017. Registration is open
Ambrus Kaposi
- [Agda] `search' format
Sergei Meshveliani
- [Agda] Some suggestions for the 'where' syntax and C-c C-,
Apostolis Xekoukoulotakis
- [Agda] Final call for papers: Trends in Functional Programming, 19-21 june 2017, University of Kent, Canterbury
Peter Achten
- [Agda] APLAS 2017 call for papers
Andreas Abel
- [Agda] Help at propositional equality proof that contains subst.
Apostolis Xekoukoulotakis
- [Agda] infix ∸-mono ?
Sergei Meshveliani
- [Agda] PPDP 2017: Call For Papers (Abstract 12 May / Paper 19 May)
Brigitte Pientka
- [Agda] Call for Contributions: Workshop on HoTT/UF (with FSCD 2017)
Anders
- [Agda] Difference between parameterized and indexed datatypes
v0id_NULL
- [Agda] Char + String
Sergei Meshveliani
- [Agda] Deadline extension may 15: Trends in Functional Programming, 19-21 june 2017, University of Kent, Canterbury
Peter Achten
- [Agda] Second call for talk proposals: Higher-Order Programming with Effects, HOPE 2017
François Pottier
- [Agda] 2nd CfP: SLE 2017 (10th ACM SIGPLAN International Conference on Software Language Engineering)
Andrei Chis
- [Agda] notes on type check performance
Sergei Meshveliani
- [Agda] Should adding eta-equality help here?
Martin Stone Davis
- [Agda] PPDP 2017: ** REVISED PAPER DEADLINE 26 May **
Brigitte Pientka
- [Agda] possible unifier bug / explain error messages?
Martin Stone Davis
- [Agda] EUTYPES summer school in Ohrid, call for applications
Tarmo Uustalu
- [Agda] Last call for talk proposals: Higher-Order Programming with Effects, HOPE 2017
François Pottier
- [Agda] strange mismatch
Sergei Meshveliani
- [Agda] constructor injectiveness
Sergei Meshveliani
- [Agda] missed wildcard pattern
Sergei Meshveliani
- [Agda] Call for participation: Trends in Functional Programming, 19-21 june 2017, University of Kent, Canterbury
Peter Achten
- [Agda] Standard library mailing list?
Jacques Carette
- [Agda] Call for participation: Trends in Functional Programming, 19-21 june 2017 AND Trends in Functional Programming in Education, 22 june 2017, University of Kent, Canterbury
Peter Achten
- [Agda] 3rd CfP: SLE 2017 (10th ACM SIGPLAN International Conference on Software Language Engineering)
Andrei Chis
- [Agda] termination with `where'
Sergei Meshveliani
- [Agda] APLAS 2017: June 13 deadline, 2nd CfP, Asian Symposium on Programming Languages and Systems
Andreas Abel
- [Agda] 1-infix-2
Sergei Meshveliani
- [Agda] Deadline Extension - SLE 2017 (10th ACM SIGPLAN International Conference on Software Language Engineering)
Andrei Chis
- [Agda] Final CFP: Workshop on Type-driven Development (TyDe '17)
Brent Yorgey
- [Agda] Type checking times and a solution.
Apostolis Xekoukoulotakis
- [Agda] matching against _::_ ?
Sergei Meshveliani
- [Agda] Possibly infinite/exponential compilation time by just calling a certain function
Jan Bracker
- [Agda] Workshop on Termination and Circular Proofs (Chambéry, 19/07)
Rodolphe Lepigre
- [Agda] When catchall does not help.
Apostolis Xekoukoulotakis
- [Agda] 1st Call for Papers IFL 2017
jurriaanhage at gmail.com
- [Agda] 1st CfP: IFL 2017 (29th Symposium on Implementation and Application of Functional Languages)
publicityifl at gmail.com
- [Agda] rewriting and parameterized modules
Ambrus Kaposi
- [Agda] unstable composition checking
Sergei Meshveliani
- [Agda] is divMod slow?
Sergei Meshveliani
- [Agda] 2nd Call for Contributions and Participation: Workshop on HoTT/UF (with FSCD 2017)
Anders Mortberg
- [Agda] timing for agda-prelude gcd
Sergei Meshveliani
- [Agda] _<_ of agda-prelude
Sergei Meshveliani
- [Agda] ICFP 2017 Student Research Competition: Call for Submissions
Sergey, Ilya
- [Agda] summing rationals
Sergei Meshveliani
- [Agda] swap in record ambiguity
Sergei Meshveliani
- [Agda] PhD offer on Integrating automated provers in proof assistants
Frédéric Blanqui
- [Agda] Some proofs by clauses
v0id_NULL
- [Agda] FLOPS2018: First CFP
Peter Thiemann
- [Agda] Proposed notation for universe polymorphism
Martín Hötzel Escardó
- [Agda] TYPES 2017 post-proceedings open call for papers
Ambrus Kaposi
- [Agda] how do I handle absurd with patterns?
Carter Schonwald
- [Agda] missing import overlap
Sergei Meshveliani
- [Agda] parameters vs indices
Thorsten Altenkirch
- [Agda] address in lib pull request
Sergei Meshveliani
- [Agda] <Programming> 2018: 2nd Call for Papers
Sylvia Grewe
- [Agda] StrictLex in library
Sergei Meshveliani
- [Agda] Postdoc positions available for ERC "CoqHoTT"
nicolas tabareau
- [Agda] updating pull request
Sergei Meshveliani
- [Agda] 2nd CfP: IFL 2017 (29th Symposium on Implementation and Application of Functional Languages)
publicityifl at gmail.com
- [Agda] ⊥-elim and proof duplication. Is there another way?
Apostolis Xekoukoulotakis
- [Agda] Call for Participation: ICFP 2017
Lindsey Kuper
- [Agda] Fixpoint in Agda
Marco Vassena
- [Agda] Some problems with K-S basis
v0id_NULL
- [Agda] divmod-unique of Agda prelude
Sergei Meshveliani
- [Agda] Call for Participation: Workshop on HoTT/UF (with FSCD 2017)
Simon Huber
- [Agda] Irrelevance and resurrection in type signatures
Matus Tejiscak
- [Agda] Instance fields
Andreas Nuyts
- [Agda] PEPM 2018 Call for Papers
PEPM Workshop
- [Agda] copyrights
Sergei Meshveliani
- [Agda] Bezonas helpon !
Serge Leblanc
- [Agda] Extended deadline: IFL 2017 (29th Symposium on Implementation and Application of Functional Languages)
publicityifl at gmail.com
- [Agda] email list reference
Sergei Meshveliani
- [Agda] installing/using 2.6.0-207bde6
Sergei Meshveliani
- [Agda] [ANNOUNCE] Agda 2.5.3 release candidate 1
Andrés Sicard-Ramírez
- [Agda] guidelines for reporting internal errors
Martin Stone Davis
- [Agda] type check cost
Sergei Meshveliani
- [Agda] Typechecking with multiple concurrent agda processes.
Apostolis Xekoukoulotakis
- [Agda] discovering verbosity options
Martin Stone Davis
- [Agda] Request of suggestion of learning material for Agda
Mario Castelán Castro
- [Agda] School and workshop on univalent mathematics, 11-15 Dec, Birmingham (UK)
Martin Escardo
- [Agda] failure to solve b/c undecidable? custom meta solvers?
Martin Stone Davis
- [Agda] [ANNOUNCE] Agda 2.5.3
Andrés Sicard-Ramírez
- [Agda] The University of Strathclyde’s Global Talent Programme - Security and Data Sciences
Robert Atkey
- [Agda] [ cubical ] : Questions on PathP on Sets.
Apostolis Xekoukoulotakis
- [Agda] Call for Presentations on Secure Compilation (PriSC Workshop @ POPL'18)
Dominique Devriese
- [Agda] common super-structure
Sergei Meshveliani
- [Agda] Should we create an issue to track the status of Cubical?
Apostolis Xekoukoulotakis
- [Agda] DoCon-A-2.00 announce
Sergei Meshveliani
- [Agda] on standard library
Sergei Meshveliani
- [Agda] Cannot apply injectivity
Sandro Stucki
- [Agda] Agda code in slides
Sergei Meshveliani
- [Agda] `with' in standard functions
Sergei Meshveliani
- [Agda] PEPM 2018 Final Call for Papers
PEPM Workshop
- [Agda] Can intuitionistic type theory express derivations of physical equations more strictly?
Hidekazu IWAKI
- [Agda] Journal of Functional Programming - Call for PhD Abstracts
Graham Hutton
- [Agda] Open call for papers: Special Issue on Homotopy Type Theory and Univalent Foundations
Anders Mortberg
- [Agda] decidable equality in algebra
Sergei Meshveliani
- [Agda] TYPES 2017 post-proceedings call for papers
Ambrus Kaposi
- [Agda] The 2018 Federated Logic Conference - Workshop Announcement
Andrzej Murawski
- [Agda] Help with With-permutations.
Apostolis Xekoukoulotakis
- [Agda] Final call for Secure Compilation presentations (PriSC Workshop @ POPL'18)
Dominique Devriese
- [Agda] No Agda AIM meeting any more?
stvienna wiener
- [Agda] Use the ring solver with an abstract ring
Chantal Keller
- [Agda] Fwd: [FP] FW: Google Internships in Programming Languages, Compilers, and Software Engineering (2018)
Andreas Abel
- [Agda] PriSC'18 deadline extended by 1 week
Dominique Devriese
- [Agda] TYPES 2017 post-proceedings DEADLINE EXTENDED
Ambrus Kaposi
- [Agda] CfP <Programming> 2018: Research Papers Third Submission Deadline
Sylvia Grewe
- [Agda] AIM XXVI - Budapest, 29 Jan -- 3 Feb 2018
Ambrus Kaposi
- [Agda] [ANNOUNCE] Standard library 0.14
Matthew Daggitt
- [Agda] [REQUEST] Help with transition from 2.5.1/2 (std-lib 0.12) to 2.5.3 (std-lib 0.14)
James McKinna
- [Agda] Call for Workshop Proposals: ICFP 2018
Lindsey Kuper
- [Agda] Call for Sponsorships: ICFP 2018
Lindsey Kuper
- [Agda] Instance arguments vs auto in Idris.
Apostolis Xekoukoulotakis
- [Agda] instance arguments and negation.
Apostolis Xekoukoulotakis
- [Agda] Agda's syntax declaration
Frederik Hanghøj Iversen
- [Agda] Installing libraries
Frederik Hanghøj Iversen
- [Agda] How do I check whether an agda term associated with a specific name relies on hole?
Anthony Cantor
- [Agda] LFMTP'18 Call for Papers
Ana Bove
- [Agda] Call for Participation for Secure Compilation Workshop (PriSC @ POPL'18)
Dominique Devriese
- [Agda] difficult termination
Sergei Meshveliani
- [Agda] Printing strings in the emacs mode
Guillaume Brunerie
- [Agda] PEPM 2018 Call for Poster/Demo Abstracts and Participation
PEPM Workshop
- [Agda] dotted patterns
Martín Hötzel Escardó
- [Agda] on `data' declaration
Sergei Meshveliani
- [Agda] Universe level checking
Martin Escardo
- [Agda] Agda Implementors' Meeting XXVI - Budapest, 29 Jan -- 3 Feb 2018
Ambrus Kaposi
- [Agda] problems installing agda master using stack
Martin Stone Davis
- [Agda] CMCS 2018: Second Call for Papers
Henning Basold
- [Agda] Fwd: Re: problems installing agda master using stack
Martin Stone Davis
- [Agda] Interactive Theorem Proving (ITP) 2018: Second CFP
Jeremy Avigad
- [Agda] Call for bids to host ITP 2019
Jeremy Avigad
- [Agda] PEPM 2018 Final Call for Poster/Demo Abstracts and Participation
PEPM Workshop
- [Agda] Non-termination help!
Martín
- [Agda] PhD positions at Nottingham
Thorsten Altenkirch
- [Agda] `<' reasoning
Sergei Meshveliani
- [Agda] CoqPL'18: call for participations and final programme
Sergey, Ilya
- [Agda] Call for Short Talks on Secure Compilation (PriSC Workshop @ POPL'18)
Dominique Devriese
- [Agda] <Programming> 2018: Call for workshop, symposium & poster submissions
Sylvia Grewe
- [Agda] How to get rid of warning
Martín Hötzel Escardó
- [Agda] Nat for termination counter
Sergei Meshveliani
- [Agda] original Nat
Sergei Meshveliani
- [Agda] numeric literals
Sergei Meshveliani
- [Agda] Call for Papers: PACMPL issue ICFP 2018
Lindsey Kuper
- [Agda] no-built-in version
Sergei Meshveliani
- [Agda] CMCS 2018: Final Call for Papers
Henning Basold
- [Agda] Font questions again
Martin Escardo
- [Agda] Naive person's questions about agda vs. haskell symbol notation
Peter Hancock
- [Agda] `let' in function signature
Sergei Meshveliani
- [Agda] Disappearing unicode in Literate Agda - XeLatex
Matthew Daggitt
- [Agda] Call for Conference Grant Applications (Inclusiveness Target Countries)
Ambrus Kaposi
Last message date:
Sun Dec 31 17:07:28 CET 2017
Archived on: Sun Dec 31 17:07:31 CET 2017
This archive was generated by
Pipermail 0.09 (Mailman edition).