2019 Archives by author

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

Starting: Tue Jan 1 03:12:47 CET 2019
Ending: Tue Dec 31 19:27:06 CET 2019
Messages: 739

• [Agda] inversion   Pierre Lescanne (en)
• [Agda] Two antagonistic definitions   Pierre Lescanne (en)
• [Agda] printing infinite structures   Setzer A.G.
• [Agda] Strangeness with corecursion   Setzer A.G.
• [Agda] summer school of proof society with proof theory of Martin-Loef Type Theory   Setzer A.G.
• [Agda] GPCE 2019: 1st Call for Papers - Athens, Greece; October 21-22   Rodin Aarssen
• [Agda] GPCE 2019: 2nd Call for Papers - Athens, Greece; October 21-22   Rodin Aarssen
• [Agda] TYPES 2019, 11-14 June 2019, Oslo: Announcement and first call for contributions   Andreas Abel
• [Agda] Emacs whitespace-mode   Andreas Abel
• [Agda] [HoTT] Re: Why do we need judgmental equality?   Andreas Abel
• [Agda] Strangeness with corecursion   Andreas Abel
• [Agda] When and where is the next AIM?   Andreas Abel
• [Agda] [Open normalization] Re: Pattern matching on irrelevant types with only one constructor?   Andreas Abel
• [Agda] the recursive definition can not terminate   Andreas Abel
• [Agda] binding variables in rewrite pragma   Andreas Abel
• [Agda] binding variables in rewrite pragma   Andreas Abel
• [Agda] termination checking loop   Andreas Abel
• [Agda] termination checking loop   Andreas Abel
• [Agda] [TFP'19] first call for papers: Trends in Functional Programming 2019, 12-14 June 2019, Vancouver, BC, CA   Peter Achten
• [Agda] [TFP'19] first call for papers: Trends in Functional Programming 2019, 12-14 June 2019, Vancouver, BC, CA (corrected dates and instructions)   Peter Achten
• [Agda] [TFP'19] second call for papers: Trends in Functional Programming 2019, 12-14 June 2019, Vancouver, BC, CA   Peter Achten
• [Agda] [TFPIE'19] Call for papers: Trends in Functional Programming in Education 2019, 11 June 2019, Vancouver, BC, CA   Peter Achten
• [Agda] [TFP'19] final call for papers (deadline extension): Trends in Functional Programming 2019, 12-14 June 2019, Vancouver, BC, CA   Peter Achten
• [Agda] [TFPIE'19] Final call for papers: Trends in Functional Programming in Education 2019, 11 June 2019, Vancouver, BC, CA   Peter Achten
• [Agda] [TFP'19 and TFPIE'19] call for participation   Peter Achten
• [Agda] [TFP'20] first call for papers: Trends in Functional Programming 2020, 13-14 February, Krakow, Poland   Peter Achten
• [Agda] [TFP'20] one month left for pre-symposium submissions for Trends in Functional Programming 2020, 13-14 February, Krakow, Poland   Peter Achten
• [Agda] [TFP'20] draft paper deadline open (January 10 2020) Trends in Functional Programming 2020, 13-14 February, Krakow, Poland   Peter Achten
• [Agda] 2-year postdoc position on type theory in Birmingham (UK)   Benedikt Ahrens
• [Agda] TC: `freshName`s are not in scope   Musa Al-hassy
• [Agda] Termination checker and rewriting   Guillaume Allais
• [Agda] Let bindings unpacking irrefutable patterns   Guillaume Allais
• [Agda] Stuck on a cubical example   Guillaume Allais
• [Agda] Strange bug   Guillaume Allais
• [Agda] printing infinite structures   Guillaume Allais
• [Agda] printing infinite structures   Guillaume Allais
• [Agda] Stuck on a cubical example   Guillaume Allais
• [Agda] Why unification fail?   Guillaume Allais
• [Agda] Stuck on a cubical example   Guillaume Allais
• [Agda] pontwise ++-cong, reverse-cong   Guillaume Allais
• [Agda] How to enforce dependencies between generalised variables   Guillaume Allais
• [Agda] fast gcd for Nat   Guillaume Allais
• [Agda] Fwd: [External] Re: Example of Finite maps with an string keys?   Guillaume Allais
• [Agda] reasoning combinator names   Guillaume Allais
• [Agda] separate definition of constructors?   Guillaume Allais
• [Agda] On termination checkers   Guillaume Allais
• [Agda] Recursive definitions over lists   Guillaume Allais
• [Agda] Using Agda in proving computer system correct   Guillaume Allais
• [Agda] Using Agda in proving computer system correct   Guillaume Allais
• [Agda] plfa preservation + progresss => eval termination checking failure in Agda 2.6.1?   Guillaume Allais
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   Guillaume Allais
• [Agda] Termination checker and rewriting   Thorsten Altenkirch
• [Agda] installing agda on windows   Thorsten Altenkirch
• [Agda] [HoTT] Re: Why do we need judgmental equality?   Thorsten Altenkirch
• [Agda] [HoTT] Re: Why do we need judgmental equality?   Thorsten Altenkirch
• [Agda] [HoTT] Re: Why do we need judgmental equality?   Thorsten Altenkirch
• [Agda] [HoTT] Re: Why do we need judgmental equality?   Thorsten Altenkirch
• [Agda] printing infinite structures   Thorsten Altenkirch
• [Agda] printing infinite structures   Thorsten Altenkirch
• [Agda] printing infinite structures   Thorsten Altenkirch
• [Agda] printing infinite structures   Thorsten Altenkirch
• [Agda] Strangeness with corecursion   Thorsten Altenkirch
• [Agda] Strangeness with corecursion   Thorsten Altenkirch
• [Agda] Defining the Delay monad as a HIT in cubical agda   Thorsten Altenkirch
• [Agda] Defining the Delay monad as a HIT in cubical agda   Thorsten Altenkirch
• [Agda] Defining the Delay monad as a HIT in cubical agda   Thorsten Altenkirch
• [Agda] When and where is the next AIM?   Thorsten Altenkirch
• [Agda] When and where is the next AIM?   Thorsten Altenkirch
• [Agda] Pattern matching on irrelevant types with only one constructor?   Thorsten Altenkirch
• [Agda] Pattern matching on irrelevant types with only one constructor?   Thorsten Altenkirch
• [Agda] Pattern matching on irrelevant types with only one constructor?   Thorsten Altenkirch
• [Agda] Pattern matching on irrelevant types with only one constructor?   Thorsten Altenkirch
• [Agda] Pattern matching on irrelevant types with only one constructor?   Thorsten Altenkirch
• [Agda] Pattern matching on irrelevant types with only one constructor?   Thorsten Altenkirch
• [Agda] problem installing agda (template Haskell ?)   Thorsten Altenkirch
• [Agda] problem installing agda (template Haskell ?)   Thorsten Altenkirch
• [Agda] problem installing agda (template Haskell ?)   Thorsten Altenkirch
• [Agda] separate definition of constructors?   Thorsten Altenkirch
• [Agda] separate definition of constructors?   Thorsten Altenkirch
• [Agda] separate definition of constructors?   Thorsten Altenkirch
• [Agda] Prop in Agda 2.6 - again   Thorsten Altenkirch
• [Agda] Types summer school 2019 at lake Ohrid   Thorsten Altenkirch
• [Agda] Types summer school 2019 at lake Ohrid   Thorsten Altenkirch
• [Agda] initial T-algebra for an endofunctor T, via sized types   Thorsten Altenkirch
• [Agda] Aquamacs path?   Thorsten Altenkirch
• [Agda] Reflection + monoiddsolver   Thorsten Altenkirch
• [Agda] Question on `unify` function in Reflection API   Kenichi Asai
• [Agda] 2 PhD studentships, MSP group, University of Strathclyde, UK   Robert Atkey
• [Agda] Totality checking in Agda   Henning Basold
• [Agda] Totality checking in Agda   Henning Basold
• [Agda] [HoTT] Re: Why do we need judgmental equality?   Henning Basold
• [Agda] printing infinite structures   Henning Basold
• [Agda] printing infinite structures   Henning Basold
• [Agda] CALCO 2019: Second Call for Papers   Henning Basold
• [Agda] Defining the Delay monad as a HIT in cubical agda   Henning Basold
• [Agda] CMCS 2020: First Call for Papers   Henning Basold
• [Agda] (Extended deadline) Formal Methods 2019 - 1st Workshop on Formal Methods for Blockchains, CFP   Bruno Bernardo
• [Agda] FMBC 2019 Call for Participation - Porto (Portugal), October 11   Bruno Bernardo
• [Agda] SPLASH 2019: 1st Combined Call for Contributions   Aggelos Biboudis
• [Agda] SPLASH 2019: 2nd Combined Call for Contributions   Aggelos Biboudis
• [Agda] SPLASH'19 Combined Call, final CfP for OOPSLA'19, Onward!   Aggelos Biboudis
• [Agda] SPLASH 2019 Combined Call for Workshop Submissions   Aggelos Biboudis
• [Agda] SPLASH 2019 Combined Call for Workshop Submissions   Aggelos Biboudis
• [Agda] SPLASH 2019 Call for Participation   Aggelos Biboudis
• [Agda] Announcement: 11th International School on Rewriting (ISR'19), 1-6 July 2019, MINES ParisTech, France   Frédéric Blanqui
• [Agda] Call for registration: 11th International School on Rewriting (ISR'19), 1-6 July 2019, MINES ParisTech, France   Frédéric Blanqui
• [Agda] New blog post: Hack your type theory with rewrite rules   Frédéric Blanqui
• [Agda] Hiding parts of proofs in Emacs Agda mode?   Guillaume Brunerie
• [Agda] agda-mode question: custom variable naming strategy for case split?   Guillaume Brunerie
• [Agda] Identifying inefficiency   Guillaume Brunerie
• [Agda] foldr _+_ vs foldl   Guillaume Brunerie
• [Agda] Platform Independent proofs.   Guillaume Brunerie
• [Agda] How does unification work?   Guillaume Brunerie
• [Agda] How does unification work?   Guillaume Brunerie
• [Agda] Agda speed in Ubuntu   Guillaume Brunerie
• [Agda] How does unification work?   Guillaume Brunerie
• [Agda] missed termination failure   Guillaume Brunerie
• [Agda] How to convert literate agda markdown to pdf with syntax-highligting   Guillermo Calderon
• [Agda] How to convert literate agda markdown to pdf with syntax-highligting   Guillermo Calderón
• [Agda] Abstract existential ?   Jacques Carette
• [Agda] Abstract existential ?   Jacques Carette
• [Agda] Abstract existential ?   Jacques Carette
• [Agda] Abstract existential ?   Jacques Carette
• [Agda] github.com/agda   Jacques Carette
• [Agda] Using Agda in proving computer system correct   Jacques Carette
• [Agda] Raw algebraic structures in the standard library   Jacques Carette
• [Agda] list comprehensions   Jacques Carette
• [Agda] Need a hand with a proof   Jacques Carette
• [Agda] separate definition of constructors?   James Chapman
• [Agda] How to obtain the reflected goal?   Liang-Ting Chen
• [Agda] How to obtain the reflected goal?   Liang-Ting Chen
• [Agda] How to obtain the reflected goal?   Liang-Ting Chen
• [Agda] Quoting mutual definition   Liang-Ting Chen
• [Agda] Quoting mutual definition   Liang-Ting Chen
• [Agda] problem installing agda (template Haskell ?)   Liang-Ting Chen
• [Agda] extendContext in reflection   Liang-Ting Chen
• [Agda] extendContext in reflection   Liang-Ting Chen
• [Agda] Using Agda in proving computer system correct   Liang-Ting Chen
• [Agda] Small Kernel   Liang-Ting Chen
• [Agda] First Call for Papers: 12th ACM SIGPLAN International Conference on Software Language Engineering (SLE 2019)   Andrei Chis
• [Agda] Second Call for Papers: 12th ACM SIGPLAN International Conference on Software Language Engineering (SLE 2019)   Andrei Chis
• [Agda] SLE 2019: Final Call for Papers - Deadline Extension; Athens, Greece; October 21-22   Andrei Chis
• [Agda] SLE 2019: Call for Endorsements - Most Influential Paper (MIP) Award   Andrei Chis
• [Agda] Termination checker and rewriting   Jesper Cockx
• [Agda] inversion   Jesper Cockx
• [Agda] Proving equality of levels with heterogeneous equality.   Jesper Cockx
• [Agda] overlapping patters   Jesper Cockx
• [Agda] Defining the Delay monad as a HIT in cubical agda   Jesper Cockx
• [Agda] Defining the Delay monad as a HIT in cubical agda   Jesper Cockx
• [Agda] Defining the Delay monad as a HIT in cubical agda   Jesper Cockx
• [Agda] Defining the Delay monad as a HIT in cubical agda   Jesper Cockx
• [Agda] Defining the Delay monad as a HIT in cubical agda   Jesper Cockx
• [Agda] Pattern matching on irrelevant types with only one constructor?   Jesper Cockx
• [Agda] Pattern matching on irrelevant types with only one constructor?   Jesper Cockx
• [Agda] Pattern matching on irrelevant types with only one constructor?   Jesper Cockx
• [Agda] Pattern matching on irrelevant types with only one constructor?   Jesper Cockx
• [Agda] TC: `freshName`s are not in scope   Jesper Cockx
• [Agda] Load libraries based on version?   Jesper Cockx
• [Agda] Type level computation in inductive types   Jesper Cockx
• [Agda] Prop in Agda 2.6 - again   Jesper Cockx
• [Agda] Prop in Agda 2.6 - again   Jesper Cockx
• [Agda] Prop in Agda 2.6 - again   Jesper Cockx
• [Agda] New blog post: Writing Agda blog posts in literate markdown   Jesper Cockx
• [Agda] How to convert literate agda markdown to pdf with syntax-highligting   Jesper Cockx
• [Agda] New blog post: Formalize All the Things (in Agda)   Jesper Cockx
• [Agda] New blog post: Hack your type theory with rewrite rules   Jesper Cockx
• [Agda] New blog post: Hack your type theory with rewrite rules   Jesper Cockx
• [Agda] New blog post: Hack your type theory with rewrite rules   Jesper Cockx
• [Agda] New blog post: Hack your type theory with rewrite rules   Jesper Cockx
• [Agda] Termination checker on commutative functions   Jesper Cockx
• [Agda] Termination checker on commutative functions   Jesper Cockx
• [Agda] New blog post: Hack your type theory with rewrite rules   Jesper Cockx
• [Agda] Reflection + monoiddsolver   Jesper Cockx
• [Agda] Small Kernel   Jesper Cockx
• [Agda] Small Kernel   Jesper Cockx
• [Agda] Small Kernel   Jesper Cockx
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   Jesper Cockx
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   Jesper Cockx
• [Agda] Hiding parts of proofs in Emacs Agda mode?   Jonathan Steven Prieto Cubides
• [Agda] 1st CFP for Certified Programs and Proofs (CPP 2020   Dominique DEVRIESE
• [Agda] CFP for Certified Programs and Proofs (CPP 2020)   Dominique DEVRIESE
• [Agda] Call for Participation: Certified Programs and Proofs (CPP 2020)   Dominique DEVRIESE
• [Agda] Hiding parts of proofs in Emacs Agda mode?   Pierre-Evariste Dagand
• [Agda] .lagda.md in emacs interactive mode   Pierre-Evariste Dagand
• [Agda] Emacs whitespace-mode   Matthew Daggitt
• [Agda] two items in standard   Matthew Daggitt
• [Agda] Fwd: Ring Solver (looking for feedback)   Matthew Daggitt
• [Agda] algebra hierarchy in library   Matthew Daggitt
• [Agda] algebra hierarchy in library   Matthew Daggitt
• [Agda] algebra hierarchy in library   Matthew Daggitt
• [Agda] Fwd: new InequalityReasoning   Matthew Daggitt
• [Agda] algebra hierarchy in library   Matthew Daggitt
• [Agda] gcd, toDecimal performance   Matthew Daggitt
• [Agda] How to enforce dependencies between generalised variables   Matthew Daggitt
• [Agda] How to enforce dependencies between generalised variables   Matthew Daggitt
• [Agda] Fwd: fastCompare for Nat   Matthew Daggitt
• [Agda] fast gcd for Nat   Matthew Daggitt
• [Agda] fast gcd for Nat   Matthew Daggitt
• [Agda] BFLib for standard   Matthew Daggitt
• [Agda] BFLib for standard   Matthew Daggitt
• [Agda] `with' vs `case'   Matthew Daggitt
• [Agda] [ANNOUNCE] Standard library 1.0   Matthew Daggitt
• [Agda] [ ANNOUNCE ] Standard Library v1.0.1   Matthew Daggitt
• [Agda] Fwd: [External] Re: Example of Finite maps with an string keys?   Matthew Daggitt
• [Agda] Pattern matching on irrelevant types with only one constructor?   Matthew Daggitt
• [Agda] Pattern matching on irrelevant types with only one constructor?   Matthew Daggitt
• [Agda] Performance tips and profiling memory usage   Matthew Daggitt
• [Agda] Performance tips and profiling memory usage   Matthew Daggitt
• [Agda] Performance tips and profiling memory usage   Matthew Daggitt
• [Agda] On termination checkers   Matthew Daggitt
• [Agda] [ANNOUNCE] Standard library v1.1   Matthew Daggitt
• [Agda] Raw algebraic structures in the standard library   Matthew Daggitt
• [Agda] GCD in future standard library   Matthew Daggitt
• [Agda] Raw algebraic structures in the standard library   Matthew Daggitt
• [Agda] Raw algebraic structures in the standard library   Matthew Daggitt
• [Agda] [ANNOUNCE] Standard library v1.2   Matthew Daggitt
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   Matthew Daggitt
• [Agda] Codata error   Nils Anders Danielsson
• [Agda] dependency graph   Nils Anders Danielsson
• [Agda] Instance search and type variables   Nils Anders Danielsson
• [Agda] Do you use postulates extensively?   Nils Anders Danielsson
• [Agda] Totality checking in Agda   Nils Anders Danielsson
• [Agda] Solver usage   Nils Anders Danielsson
• [Agda] Totality checking in Agda   Nils Anders Danielsson
• [Agda] Totality checking in Agda   Nils Anders Danielsson
• [Agda] Solver usage   Nils Anders Danielsson
• [Agda] Termination checker and rewriting   Nils Anders Danielsson
• [Agda] Question about coinductive types   Nils Anders Danielsson
• [Agda] installing agda on windows   Nils Anders Danielsson
• [Agda] installing agda on windows   Nils Anders Danielsson
• [Agda] arch inux packaging error?   Nils Anders Danielsson
• [Agda] Strangeness with corecursion   Nils Anders Danielsson
• [Agda] arch inux packaging error?   Nils Anders Danielsson
• [Agda] Try It Online   Nils Anders Danielsson
• [Agda] .lagda.md in emacs interactive mode   Nils Anders Danielsson
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1   Nils Anders Danielsson
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1   Nils Anders Danielsson
• [Agda] Defining the Delay monad as a HIT in cubical agda   Nils Anders Danielsson
• [Agda] Defining the Delay monad as a HIT in cubical agda   Nils Anders Danielsson
• [Agda] Defining the Delay monad as a HIT in cubical agda   Nils Anders Danielsson
• [Agda] Performance tips and profiling memory usage   Nils Anders Danielsson
• [Agda] Performance tips and profiling memory usage   Nils Anders Danielsson
• [Agda] HITs without paths   Nils Anders Danielsson
• [Agda] separate definition of constructors?   Nils Anders Danielsson
• [Agda] On termination checkers   Nils Anders Danielsson
• [Agda] Agda speed in Ubuntu   Nils Anders Danielsson
• [Agda] Using Agda in proving computer system correct   Nils Anders Danielsson
• [Agda] Using Agda in proving computer system correct   Nils Anders Danielsson
• [Agda] plfa preservation + progresss => eval termination checking failure in Agda 2.6.1?   Nils Anders Danielsson
• [Agda] Agda speed in Ubuntu   Nils Anders Danielsson
• [Agda] Agda speed in Ubuntu   Nils Anders Danielsson
• [Agda] Raw algebraic structures in the standard library   Nils Anders Danielsson
• [Agda] using agda   Nils Anders Danielsson
• [Agda] How does unification work?   Nils Anders Danielsson
• [Agda] agda ghc backend executable (re)location   Nils Anders Danielsson
• [Agda] question about termination checker   Nils Anders Danielsson
• [Agda] Undocumented (Recursive?) Positivity Checking   Nils Anders Danielsson
• [Agda] Undocumented (Recursive?) Positivity Checking   Nils Anders Danielsson
• [Agda] Undocumented (Recursive?) Positivity Checking   Nils Anders Danielsson
• [Agda] Agda2 emacs mode - yellow highlighting   Nils Anders Danielsson
• [Agda] usage of a definition   Nils Anders Danielsson
• [Agda] syntactic sugar parameters   Nils Anders Danielsson
• [Agda] How to prove termination for the iterated halving function over the rationals?   Nils Anders Danielsson
• [Agda] Contributing: good first issues   Nils Anders Danielsson
• [Agda] agda ghc backend executable (re)location   Martin Stone Davis
• [Agda] using agda   Jeremy Dawson
• [Agda] using agda   Jeremy Dawson
• [Agda] using agda   Jeremy Dawson
• [Agda] using agda   Jeremy Dawson
• [Agda] Unification failure when using Pointwise-length   Deyaaeldeen
• [Agda] Sized types question   Deyaaeldeen
• [Agda] Totality checking in Agda   Marko Dimjašević
• [Agda] Totality checking in Agda   Marko Dimjašević
• [Agda] Totality checking in Agda   Marko Dimjašević
• [Agda] Using Agda in proving computer system correct   Marko Dimjašević
• [Agda] Using Agda in proving computer system correct   Marko Dimjašević
• [Agda] Searching for a state machine library   Marko Dimjašević
• [Agda] Contributing: good first issues   Marko Dimjašević
• [Agda] Contributing: good first issues   Marko Dimjašević
• [Agda] Contributing: good first issues   Marko Dimjašević
• [Agda] Defining the Delay monad as a HIT in cubical agda   Dan Doel
• [Agda] Defining the Delay monad as a HIT in cubical agda   Dan Doel
• [Agda] Defining the Delay monad as a HIT in cubical agda   Dan Doel
• [Agda] Undocumented (Recursive?) Positivity Checking   Yotam Dvir
• [Agda] Undocumented (Recursive?) Positivity Checking   Yotam Dvir
• [Agda] Small Kernel   Yotam Dvir
• [Agda] ECI 2020: DEADLINE EXTENSION (22 Nov 19) - Call for course proposals   Alejandro Díaz-Caro
• [Agda] Instance Search fails with parameterized modules?   Joey Eremondi
• [Agda] Instance Search fails with parameterized modules?   Joey Eremondi
• [Agda] dependency graph   Martin Escardo
• [Agda] dependency graph   Martin Escardo
• [Agda] Do you use postulates extensively?   Martin Escardo
• [Agda] Midlands Graduate School 2019 in the Foundations of Computing Science   Martin Escardo
• [Agda] Hiding parts of proofs in Emacs Agda mode?   Martin Escardo
• [Agda] Abstract existential ?   Martin Escardo
• [Agda] Abstract existential ?   Martin Escardo
• [Agda] .lagda.md in emacs interactive mode   Martin Escardo
• [Agda] .lagda.md in emacs interactive mode   Martin Escardo
• [Agda] Case split on λ()   Martin Escardo
• [Agda] Case split on λ()   Martin Escardo
• [Agda] Case split on λ()   Martin Escardo
• [Agda] Case split on λ()   Martin Escardo
• [Agda] Univalent foundations in Agda lecture notes   Martin Escardo
• [Agda] Univalent foundations in Agda lecture notes   Martin Escardo
• [Agda] Identifying inefficiency   Martin Escardo
• [Agda] Identifying inefficiency   Martin Escardo
• [Agda] Identifying inefficiency   Martin Escardo
• [Agda] Identifying inefficiency   Martin Escardo
• [Agda] Defining the Delay monad as a HIT in cubical agda   Martin Escardo
• [Agda] Identifying inefficiency   Martin Escardo
• [Agda] Two antagonistic definitions   Martin Escardo
• [Agda] Agda speed in Ubuntu   Martin Escardo
• [Agda] Agda speed in Ubuntu   Martin Escardo
• [Agda] Agda speed in Ubuntu   Martin Escardo
• [Agda] Agda speed in Ubuntu   Martin Escardo
• [Agda] Agda speed in Ubuntu   Martin Escardo
• [Agda] Agda speed in Ubuntu   Martin Escardo
• [Agda] Agda speed in Ubuntu   Martin Escardo
• [Agda] PPDP 2019 CFP - Principles and Practice of Declarative Programming   František Farka
• [Agda] Postdoc Position at the University of Minnesota   Favonia
• [Agda] Multiple tenure-track positions at the University of Minnesota   Favonia
• [Agda] Postdoctoral position in Compositional Game Theory at Univ. of Strathclyde   Fredrik Nordvall Forsberg
• [Agda] Scottish Programming Languages and Verification Summer School   Fredrik Nordvall Forsberg
• [Agda] Final Call for Participation: Scottish Programming Languages and Verification Summer School   Fredrik Nordvall Forsberg
• [Agda] Termination checker and rewriting   Guillaume GENESTIER
• [Agda] New blog post: Writing Agda blog posts in literate markdown   Dr. ÉRDI Gergő
• [Agda] ARRAY workshop at PLDI 2019, submissions due 8th April   Jeremy Gibbons
• [Agda] How to prove termination for the iterated halving function over the rationals?   Marko Grdinic
• [Agda] installing agda-master with cabal on ubuntu   Oleg Grenrus
• [Agda] PhD position in type theory at the University of Bergen   Håkon Robbestad Gylterud
• [Agda] Call for papers for IFL 2019 (Implementation and Application of Functional Languages)   Jurriaan Hage
• [Agda] Final call for regular papers for IFL 2019 (Implementation and Application of Functional Languages)   Jurriaan Hage
• [Agda] Final call for draft papers for IFL 2019 (Implementation and Application of Functional Languages)   Jurriaan Hage
• [Agda] First call for participation for IFL 2019 (Implementation and Application of Functional Languages)   Jurriaan Hage
• [Agda] First call for draft papers for TFPIE 2020 (Trends in Functional Programming in Education)   Jurriaan Hage
• [Agda] Second call for draft papers for TFPIE 2020 (Trends in Functional Programming in Education)   Jurriaan Hage
• [Agda] Third call for draft papers for TFPIE 2020 (Trends in Functional Programming in Education)   Jurriaan Hage
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 2   Peter Hancock
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 2   Peter Hancock
• [Agda] Small Kernel   Peter Hancock
• [Agda] Small Kernel   Peter Hancock
• [Agda] Platform Independent proofs.   Philipp Hausmann
• [Agda] Hiding parts of proofs in Emacs Agda mode?   Jason -Zhong Sheng- Hu
• [Agda] Let bindings unpacking irrefutable patterns   Jason -Zhong Sheng- Hu
• [Agda] Let bindings unpacking irrefutable patterns   Jason -Zhong Sheng- Hu
• [Agda] A question on a highlighted expression in Emacs   Jason -Zhong Sheng- Hu
• [Agda] A question on a highlighted expression in Emacs   Jason -Zhong Sheng- Hu
• [Agda] Proving equality of levels with heterogeneous equality.   Jason -Zhong Sheng- Hu
• [Agda] Case split on λ()   Jason -Zhong Sheng- Hu
• [Agda] Case split on λ()   Jason -Zhong Sheng- Hu
• [Agda] inspect idiom with more than one argument   Jason -Zhong Sheng- Hu
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1   Jason -Zhong Sheng- Hu
• [Agda] What do "constraints" mean?   Jason -Zhong Sheng- Hu
• [Agda] Load libraries based on version?   Jason -Zhong Sheng- Hu
• [Agda] Load libraries based on version?   Jason -Zhong Sheng- Hu
• [Agda] Load libraries based on version?   Jason -Zhong Sheng- Hu
• [Agda] Type of Natural numbers representations   Jason -Zhong Sheng- Hu
• [Agda] Using Agda in proving computer system correct   Jason -Zhong Sheng- Hu
• [Agda] good CSS?   Jason -Zhong Sheng- Hu
• [Agda] good CSS?   Jason -Zhong Sheng- Hu
• [Agda] Agda Logo Poll Results   Jason -Zhong Sheng- Hu
• [Agda] copattern split in Emacs?   Jason -Zhong Sheng- Hu
• [Agda] copattern split in Emacs?   Jason -Zhong Sheng- Hu
• [Agda] usage of a definition   Jason -Zhong Sheng- Hu
• [Agda] Need a hand with a proof   Jason -Zhong Sheng- Hu
• [Agda] 10 PhD studentships in Nottingham   Graham Hutton
• [Agda] Call for Papers, MPC 2019, Portugal   Graham Hutton
• [Agda] Second call for papers, MPC 2019, Portugal   Graham Hutton
• [Agda] MPC 2019 final call for papers - submissions due 3rd May   Graham Hutton
• [Agda] MPC 2019 deadline extension   Graham Hutton
• [Agda] Journal of Functional Programming - Call for PhD Abstracts   Graham Hutton
• [Agda] Assistant/Associate Professorships in Nottingham   Graham Hutton
• [Agda] Multiple Assistant/Associate Professorships in Nottingham (deadline 8th July 2019)   Graham Hutton
• [Agda] MPC 2019 - Call for Participation   Graham Hutton
• [Agda] MPC 2019 - Call for Participation   Graham Hutton
• [Agda] MPC 2019 - final call for participation   Graham Hutton
• [Agda] Journal of Functional Programming - Call for PhD Abstracts   Graham Hutton
• [Agda] 10 PhD studentships in Nottingham   Graham Hutton
• [Agda] Question about coinductive types   Pierre Hyvernat
• [Agda] Question about coinductive types   Pierre Hyvernat
• [Agda] Error in pattern matching dependent family   Pierre Hyvernat
• [Agda] How can I prove algebraic laws of HITs in Cubical Agda?   Hiromi ISHII
• [Agda] How can I prove algebraic laws of HITs in Cubical Agda?   Hiromi ISHII
• [Agda] CIFRE PhD thesis position in Siemens Mobility, Chatillon   Danko Ilik
• [Agda] Question on `unify` function in Reflection API   Chiaki Ishio
• [Agda] Defining the Delay monad as a HIT in cubical agda   Tom Jack
• [Agda] Stuck on a cubical example   Wolfram Kahl
• [Agda] Identifying inefficiency   Wolfram Kahl
• [Agda] Performance tips and profiling memory usage   Wolfram Kahl
• [Agda] Call for talks (with travel funding): EUTypes WG meeting in Krakow, 23-24 February 2019   Ambrus Kaposi
• [Agda] PhD studentship in Budapest   Ambrus Kaposi
• [Agda] separate definition of constructors?   Ambrus Kaposi
• [Agda] Call for Conference Grant Applications (Inclusiveness Target Countries)   Ambrus Kaposi
• [Agda] Call for Conference Grant Applications (Inclusiveness Target Countries)   Ambrus Kaposi
• [Agda] Termination checker on commutative functions   Jacek Karwowski
• [Agda] Termination checker on commutative functions   Jacek Karwowski
• [Agda] PxTP 2019 - Call for Papers   Chantal Keller
• [Agda] PxTP 2019 - 2nd Call for Papers   Chantal Keller
• [Agda] PxTP 2019 - Last Call for Papers   Chantal Keller
• [Agda] PhD, postdoc and research engineer positions at Universite Paris-Saclay/Inria   Chantal Keller
• [Agda] Ring Solver (looking for feedback)   Donnacha Oisín Kidney
• [Agda] Summer School on Nominal Techniques: FoPSS 2019   Bartek Klin
• [Agda] FoPSS'19: Summer School on Foundations of Programming and Software Systems   Bartek Klin
• [Agda] Bx 2019 Second Call for Papers (Workshop on Bidirectional Transformations)   Josh Ko
• [Agda] Bx 2019 Call for Participation   Josh Ko
• [Agda] Defining the Delay monad as a HIT in cubical agda   Nicolai Kraus
• [Agda] Defining the Delay monad as a HIT in cubical agda   Nicolai Kraus
• [Agda] Defining the Delay monad as a HIT in cubical agda   Nicolai Kraus
• [Agda] Defining the Delay monad as a HIT in cubical agda   Nicolai Kraus
• [Agda] Defining the Delay monad as a HIT in cubical agda   Nicolai Kraus
• [Agda] Defining the Delay monad as a HIT in cubical agda   Nicolai Kraus
• [Agda] Defining the Delay monad as a HIT in cubical agda   Nicolai Kraus
• [Agda] Prop in Agda 2.6   Nicolai Kraus
• [Agda] PhD position in homotopy type theory at Birmingham   Nicolai Kraus
• [Agda] Call for scholarship applications: PLMW @ POPL 2020   Robbert Krebbers
• [Agda] plfa preservation + progresss => eval termination checking failure in Agda 2.6.1?   Dan Krejsa
• [Agda] Abstract existential ?   Neel Krishnaswami
• [Agda] Why unification fail?   Serge Leblanc
• [Agda] Why unification fail?   Serge Leblanc
• [Agda] Why unification fail?   Serge Leblanc
• [Agda] Example of Finite maps with an string keys?   Serge Leblanc
• [Agda] [External] Re: Example of Finite maps with an string keys?   Serge Leblanc
• [Agda] Case split on λ()   Marcus Christian Lehmann
• [Agda] Case split on λ()   Marcus Christian Lehmann
• [Agda] Case split on λ()   Marcus Christian Lehmann
• [Agda] Case split on λ()   Marcus Christian Lehmann
• [Agda] Case split on λ()   Marcus Christian Lehmann
• [Agda] Case split on λ()   Marcus Christian Lehmann
• [Agda] cabal cannot install Agda 2.6.0   Pierre Lescanne
• [Agda] cabal cannot install Agda 2.6.0   Pierre Lescanne
• [Agda] Sized Types: Run-length Encoding Example   Jannis Limperg
• [Agda] Sized Types: Run-length Encoding Example   Craig McLaughlin
• [Agda] Example of Finite maps with an string keys?   Orestis Melkonian
• [Agda] Performance tips and profiling memory usage   Orestis Melkonian
• [Agda] overlapping _∷_, []   Orestis Melkonian
• [Agda] Codata error   Sergei Meshveliani
• [Agda] Do you use postulates extensively?   Sergei Meshveliani
• [Agda] Do you use postulates extensively?   Sergei Meshveliani
• [Agda] Do you use postulates extensively?   Sergei Meshveliani
• [Agda] Do you use postulates extensively?   Sergei Meshveliani
• [Agda] Solver usage   Sergei Meshveliani
• [Agda] Solver usage   Sergei Meshveliani
• [Agda] two items in standard   Sergei Meshveliani
• [Agda] interactive Bin arith performance   Sergei Meshveliani
• [Agda] interactive Bin arith performance   Sergei Meshveliani
• [Agda] interactive Bin arith performance   Sergei Meshveliani
• [Agda] interactive Bin arith performance   Sergei Meshveliani
• [Agda] interactive Bin arith performance   Sergei Meshveliani
• [Agda] interactive Bin arith performance   Sergei Meshveliani
• [Agda] interactive Bin arith performance   Sergei Meshveliani
• [Agda] interactive Bin arith performance   Sergei Meshveliani
• [Agda] interactive Bin arith performance   Sergei Meshveliani
• [Agda] algebra hierarchy in library   Sergei Meshveliani
• [Agda] algebra hierarchy in library   Sergei Meshveliani
• [Agda] algebra hierarchy in library   Sergei Meshveliani
• [Agda] algebra hierarchy in library   Sergei Meshveliani
• [Agda] algebra hierarchy in library   Sergei Meshveliani
• [Agda] pontwise ++-cong, reverse-cong   Sergei Meshveliani
• [Agda] pontwise ++-cong, reverse-cong   Sergei Meshveliani
• [Agda] overlapping patters   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1   Sergei Meshveliani
• [Agda] algebra hierarchy in library   Sergei Meshveliani
• [Agda] new InequalityReasoning   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1   Sergei Meshveliani
• [Agda] new InequalityReasoning   Sergei Meshveliani
• [Agda] algebra hierarchy in library   Sergei Meshveliani
• [Agda] built-in divMod   Sergei Meshveliani
• [Agda] built-in divMod   Sergei Meshveliani
• [Agda] algebra hierarchy in library   Sergei Meshveliani
• [Agda] Univalent foundations in Agda lecture notes   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1   Sergei Meshveliani
• [Agda] gcd, toDecimal performance   Sergei Meshveliani
• [Agda] gcd, toDecimal performance   Sergei Meshveliani
• [Agda] fastCompare for Nat   Sergei Meshveliani
• [Agda] fast gcd for Nat   Sergei Meshveliani
• [Agda] foldr _+_ vs foldl   Sergei Meshveliani
• [Agda] foldr _+_ vs foldl   Sergei Meshveliani
• [Agda] foldr _+_ vs foldl   Sergei Meshveliani
• [Agda] BFLib for standard   Sergei Meshveliani
• [Agda] BFLib for standard   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 2   Sergei Meshveliani
• [Agda] `with' fail   Sergei Meshveliani
• [Agda] `with' vs `case'   Sergei Meshveliani
• [Agda] Performance tips and profiling memory usage   Sergei Meshveliani
• [Agda] BF library announcement   Sergei Meshveliani
• [Agda] reasoning combinator names   Sergei Meshveliani
• [Agda] reasoning combinator names   Sergei Meshveliani
• [Agda] Proving equality of levels with heterogeneous equality.   Stefan Monnier
• [Agda] Pattern matching on irrelevant types with only one constructor?   Stefan Monnier
• [Agda] Question about coinductive types   Anders Mortberg
• [Agda] Stuck on a cubical example   Anders Mortberg
• [Agda] Stuck on a cubical example   Anders Mortberg
• [Agda] PhD position in Computational Mathematics at Stockholm University   Anders Mortberg
• [Agda] APLAS 2019 Call for Papers   Shin-Cheng Mu
• [Agda] FLOPS 2020 Final Call for papers   Shin-Cheng Mu
• [Agda] FLOPS 2020 CFP: Deadline Extension!   Shin-Cheng Mu
• [Agda] FLOPS 2020 First Call for papers   Keisuke Nakano
• [Agda] MSFP 2020 - First Call for Papers   Max New
• [Agda] interactive Bin arith performance   Ulf Norell
• [Agda] interactive Bin arith performance   Ulf Norell
• [Agda] interactive Bin arith performance   Ulf Norell
• [Agda] interactive Bin arith performance   Ulf Norell
• [Agda] interactive Bin arith performance   Ulf Norell
• [Agda] installing agda on windows   Ulf Norell
• [Agda] built-in divMod   Ulf Norell
• [Agda] built-in divMod   Ulf Norell
• [Agda] How to enforce dependencies between generalised variables   Ulf Norell
• [Agda] foldr _+_ vs foldl   Ulf Norell
• [Agda] How to obtain the reflected goal?   Ulf Norell
• [Agda] How to obtain the reflected goal?   Ulf Norell
• [Agda] Quoting mutual definition   Ulf Norell
• [Agda] github.com/agda   Ulf Norell
• [Agda] How does unification work?   Ulf Norell
• [Agda] Question on `unify` function in Reflection API   Ulf Norell
• [Agda] Reflection + monoiddsolver   Ulf Norell
• [Agda] Instance Search fails with parameterized modules?   Ulf Norell
• [Agda] Contributing: good first issues   Ulf Norell
• [Agda] ENTROPY 2019: Call for Papers - Co-located with EuroS&P'19   David Nowak
• [Agda] ENTROPY 2019: Second Call for Papers - Co-located with EuroS&P'19   David Nowak
• [Agda] ENTROPY 2019: Deadline Extension -- Final Call for Papers   David Nowak
• [Agda] ENTROPY 2019: Call for Participation - Co-located with EuroS&P'19   David Nowak
• [Agda] Abstract existential ?   Andreas Nuyts
• [Agda] Abstract existential ?   Andreas Nuyts
• [Agda] Let bindings unpacking irrefutable patterns   Andreas Nuyts
• [Agda] Postdoctoral positions in Trustworthy Systems at UNSW   Liam O'Connor
• [Agda] PhD positions with Cogent and Trustworthy Systems   Liam O'Connor
• [Agda] How to make chain of reasoning explicit in Agda   Herminie Pagel
• [Agda] Type of Natural numbers representations   Herminie Pagel
• [Agda] syntactic sugar parameters   Herminie Pagel
• [Agda] Contributing: good first issues   Herminie Pagel
• [Agda] Contributing: good first issues   Herminie Pagel
• [Agda] agda-spec horizon   Herminie Pagel
• [Agda] How to formalize synonym types?   Herminie Pagel
• [Agda] Hiding parts of proofs in Emacs Agda mode?   Erik Palmgren
• [Agda] Hiding parts of proofs in Emacs Agda mode?   Erik Palmgren
• [Agda] A setoid model of extensional Martin-Löf type theory in Agda   Erik Palmgren
• [Agda] How does unification work?   Erik Palmgren
• [Agda] How does unification work?   Erik Palmgren
• [Agda] Fwd: Programming with well-founded/sized recursion   Patricia Peratto
• [Agda] Instance search and type variables   Pavel Perikov
• [Agda] Abstract existential ?   Andrew Pitts
• [Agda] Prop in Agda 2.6   Andrew Pitts
• [Agda] Prop in Agda 2.6   Andrew Pitts
• [Agda] Prop in Agda 2.6 - again   Andrew Pitts
• [Agda] Prop in Agda 2.6 - again   Andrew Pitts
• [Agda] Prop in Agda 2.6 - again   Andrew Pitts
• [Agda] On termination checkers   Andrew Pitts
• [Agda] On termination checkers   Andrew Pitts
• [Agda] On termination checkers   Andrew Pitts
• [Agda] initial T-algebra for an endofunctor T, via sized types   Andrew Pitts
• [Agda] initial T-algebra for an endofunctor T, via sized types   Andrew Pitts
• [Agda] initial T-algebra for an endofunctor T, via sized types   Andrew Pitts
• [Agda] Agda2 emacs mode - yellow highlighting   Andrew Pitts
• [Agda] printing infinite structures   Paulo Pizani
• [Agda] FroCoS 2019 (London): DEADLINE EXTENSION and final call for papers   Andrei Popescu
• [Agda] TABLEAUX 2019 (London): DEADLINE EXTENSION and final call for papers   Andrei Popescu
• [Agda] FroCoS and TABLEAUX 2019 (London): SECOND (AND FINAL) DEADLINE EXTENSION   Andrei Popescu
• [Agda] FroCoS 2019 and TABLEAUX 2019 (London, September 2-6): call for participation   Andrei Popescu
• [Agda] FroCoS-12 and TABLEAUX-28, London, September 2-6: second call for participation (early registration closes on August 21)   Andrei Popescu
• [Agda] Last minute proposals for the Agda logo   Nicolas Pouillard
• [Agda] About the logo poll and its issues   Nicolas Pouillard
• [Agda] About the logo poll and its issues   Nicolas Pouillard
• [Agda] Agda Logo Poll Results   Nicolas Pouillard
• [Agda] Agda Logo Poll Results   Nicolas Pouillard
• [Agda] PEPM 2020 Call for Papers   Casper Bach Poulsen
• [Agda] PEPM 2020: DEADLINE EXTENSION to 25 Oct   Casper Bach Poulsen
• [Agda] PEPM 2020 Call for Participation   Casper Bach Poulsen
• [Agda] New blog post: Hack your type theory with rewrite rules   Benjamin Price
• [Agda] installing agda on windows   Xuanrui Qi
• [Agda] arch inux packaging error?   Xuanrui Qi
• [Agda] inspect idiom with more than one argument   Xuanrui Qi
• [Agda] inspect idiom with more than one argument   Xuanrui Qi
• [Agda] Programming with well-founded/sized recursion   Xuanrui Qi
• [Agda] Using Agda in proving computer system correct   Xuanrui Qi
• [Agda] Using Agda in proving computer system correct   Xuanrui Qi
• [Agda] Small Kernel   Xuanrui Qi
• [Agda] installing agda-master with cabal on ubuntu   Andres Sicard Ramirez
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1   Andres Sicard Ramirez
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1   Andres Sicard Ramirez
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1   Andres Sicard Ramirez
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1   Andres Sicard Ramirez
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 2   Andres Sicard Ramirez
• [Agda] [ANNOUNCE] Agda 2.6.0 release candidate 2   Andres Sicard Ramirez
• [Agda] [ANNOUNCE] Agda 2.6.0   Andres Sicard Ramirez
• [Agda] [ Poll ] Maintain support for GHC 7.10.3   Andres Sicard Ramirez
• [Agda] [ANNOUNCE] Agda 2.6.0.1   Andres Sicard Ramirez
• [Agda] problem installing agda (template Haskell ?)   Andres Sicard Ramirez
• [Agda] problem installing agda (template Haskell ?)   Andres Sicard Ramirez
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   Andres Sicard Ramirez
• [Agda] 2nd CFP: 3rd International Workshop on User-Oriented Logic Paradigms   Christos Rodosthenous
• [Agda] 2nd CFP: 3rd International Workshop on User-Oriented Logic Paradigms   Christos Rodosthenous
• [Agda] Proving equality of levels with heterogeneous equality.   Roman
• [Agda] separate definition of constructors?   Roman
• [Agda] Using Agda in proving computer system correct   Roman
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   Christian Sattler
• [Agda] How can I prove algebraic laws of HITs in Cubical Agda?   Caryo Scelus
• [Agda] using agda   Caryo Scelus
• [Agda] using agda   Caryo Scelus
• [Agda] arch inux packaging error?   Marko Schuetz-Schmuck
• [Agda] arch inux packaging error?   Marko Schuetz-Schmuck
• [Agda] arch inux packaging error?   Marko Schuetz-Schmuck
• [Agda] Programming with well-founded/sized recursion   Filippo Sestini
• [Agda] Aquamacs path?   Filippo Sestini
• [Agda] [HoTT] Re: Why do we need judgmental equality?   Michael Shulman
• [Agda] binding variables in rewrite pragma   Michael Shulman
• [Agda] irrelevant contradiction?   Siek, Jeremy
• [Agda] irrelevant contradiction?   Siek, Jeremy
• [Agda] Using Agda in proving computer system correct   Matthieu Sozeau
• [Agda] [HoTT] Re: Why do we need judgmental equality?   Bas Spitters
• [Agda] PhD vacancy in Formally verified crypto at Aarhus   Bas Spitters
• [Agda] PhD and Postdoc positions in Aarhus (DK)   Bas Spitters
• [Agda] New blog post: Hack your type theory with rewrite rules   Bas Spitters
• [Agda] Defining the Delay monad as a HIT in cubical agda   Jon Sterling
• [Agda] Pattern matching on irrelevant types with only one constructor?   Jon Sterling
• [Agda] Pattern matching on irrelevant types with only one constructor?   Jon Sterling
• [Agda] Pattern matching on irrelevant types with only one constructor?   Jon Sterling
• [Agda] Prop in Agda 2.6   Jon Sterling
• [Agda] Prop in Agda 2.6   Jon Sterling
• [Agda] Prop in Agda 2.6   Jon Sterling
• [Agda] separate definition of constructors?   Jon Sterling
• [Agda] separate definition of constructors?   Jon Sterling
• [Agda] Using Agda in proving computer system correct   Jon Sterling
• [Agda] New blog post: Hack your type theory with rewrite rules   Jon Sterling
• [Agda] New blog post: Hack your type theory with rewrite rules   Jon Sterling
• [Agda] [HoTT] Re: Why do we need judgmental equality?   Thomas Streicher
• [Agda] installing agda on windows   Aaron Stump
• [Agda] postdoc opportunity on Cedille project   Aaron Stump
• [Agda] [External] Re: Example of Finite maps with an string keys?   Aaron Stump
• [Agda] rewriting reveals extra arguments   Aaron Stump
• [Agda] postdoc position   Aaron Stump
• [Agda] Vacancies for six Assistant Professor positions at Utrecht University   Swierstra, W.S. (Wouter)
• [Agda] Utrecht Summer School on Advanced Functional Programming   Swierstra, W.S. (Wouter)
• [Agda] Second Call for Papers: PACMPL issue ICFP 2019   Sam Tobin-Hochstadt
• [Agda] Third Call for Papers: PACMPL issue ICFP 2019   Sam Tobin-Hochstadt
• [Agda] Call for Submissions: ICFP Student Research Competition   Sam Tobin-Hochstadt
• [Agda] Call for Tutorial Proposals: ICFP 2019   Sam Tobin-Hochstadt
• [Agda] PLMW at ICFP: Call for Scholarship Applications (due 17 May)   Sam Tobin-Hochstadt
• [Agda] Second Call for Tutorial Proposals: ICFP 2019   Sam Tobin-Hochstadt
• [Agda] Second Call for Submissions: ICFP Student Research Competition   Sam Tobin-Hochstadt
• [Agda] Call for Participation: ICFP 2019   Sam Tobin-Hochstadt
• [Agda] Second Call for Participation: ICFP 2019   Sam Tobin-Hochstadt
• [Agda] Call for Workshop Proposals: ICFP 2020   Sam Tobin-Hochstadt
• [Agda] ETAPS 2020 2nd joint call for papers   Tarmo Uustalu
• [Agda] NWPT 2019 submission deadline extended   Tarmo Uustalu
• [Agda] First ETAPS Doctoral Dissertation Award   Tarmo Uustalu
• [Agda] Question about coinductive types   Andrea Vezzosi
• [Agda] Defining the Delay monad as a HIT in cubical agda   Andrea Vezzosi
• [Agda] Defining the Delay monad as a HIT in cubical agda   Andrea Vezzosi
• [Agda] Defining the Delay monad as a HIT in cubical agda   Andrea Vezzosi
• [Agda] Identifying inefficiency   Andrea Vezzosi
• [Agda] Defining the Delay monad as a HIT in cubical agda   Andrea Vezzosi
• [Agda] Pattern matching on irrelevant types with only one constructor?   Andrea Vezzosi
• [Agda] Strange bug   Philip Wadler
• [Agda] Strange bug   Philip Wadler
• [Agda] Recursive definitions over lists   Philip Wadler
• [Agda] Recursive definitions over lists   Philip Wadler
• [Agda] good CSS?   Philip Wadler
• [Agda] Error in pattern matching dependent family   James Wood
• [Agda] Strangeness with corecursion   James Wood
• [Agda] It is hard to understand the agda error message   James Wood
• [Agda] copattern split in Emacs?   James Wood
• [Agda] syntactic sugar parameters   James Wood
• [Agda] list comprehensions   James Wood
• [Agda] overlapping _∷_, []   James Wood
• [Agda] Unification failure when using Pointwise-length   Apostolis Xekoukoulotakis
• [Agda] Do you use postulates extensively?   Apostolis Xekoukoulotakis
• [Agda] Do you use postulates extensively?   Apostolis Xekoukoulotakis
• [Agda] Do you use postulates extensively?   Apostolis Xekoukoulotakis
• [Agda] Do you use postulates extensively?   Apostolis Xekoukoulotakis
• [Agda] Do you use postulates extensively?   Apostolis Xekoukoulotakis
• [Agda] Do you use postulates extensively?   Apostolis Xekoukoulotakis
• [Agda] How to write proofs by Leslie Lamport : Hierarchical structures   Apostolis Xekoukoulotakis
• [Agda] printing infinite structures   Apostolis Xekoukoulotakis
• [Agda] A question on a highlighted expression in Emacs   Apostolis Xekoukoulotakis
• [Agda] Proving equality of levels with heterogeneous equality.   Apostolis Xekoukoulotakis
• [Agda] Case split on λ()   Apostolis Xekoukoulotakis
• [Agda] foldr _+_ vs foldl   Apostolis Xekoukoulotakis
• [Agda] foldr _+_ vs foldl   Apostolis Xekoukoulotakis
• [Agda] Quoting mutual definition   Apostolis Xekoukoulotakis
• [Agda] When and where is the next AIM?   Apostolis Xekoukoulotakis
• [Agda] Platform Independent proofs.   Apostolis Xekoukoulotakis
• [Agda] Platform Independent proofs.   Apostolis Xekoukoulotakis
• [Agda] Selectively capturing variables from the exterior context.(?)   Apostolis Xekoukoulotakis
• [Agda] Repository with executable agda code.   Apostolis Xekoukoulotakis
• [Agda] New blog post: Hack your type theory with rewrite rules   Apostolis Xekoukoulotakis
• [Agda] irrelevant contradiction?   Apostolis Xekoukoulotakis
• [Agda] 4th autumn school "Proof and Computation"   Chuangjie Xu
• [Agda] 4th autumn school "Proof and Computation"   Chuangjie Xu
• [Agda] Agda Implementors' Meeting XXX - Munich, 11-17 September 2019   Chuangjie Xu
• [Agda] Agda Implementors' Meeting XXX - Munich, 11-17 September 2019   Chuangjie Xu
• [Agda] Workshop on Foundations and Applications of Univalent Mathematics, 18-20 December 2019, Herrsching   Chuangjie Xu
• [Agda] Metaprogramming Summer School (August 2019): call for applications   Jeremy Yallop
• [Agda] agda-mode question: custom variable naming strategy for case split?   Noam Zeilberger
• [Agda] agda-mode question: custom variable naming strategy for case split?   Noam Zeilberger
• [Agda] agda-mode question: custom variable naming strategy for case split?   Noam Zeilberger
• [Agda] Load libraries based on version?   a.j.rouvoet
• [Agda] Small Kernel   a.j.rouvoet
• [Agda] ITRS 2020 Call for contributions   Ugo de'Liguoro
• [Agda] TYPES 2020 - Call for contributions   Ugo de'Liguoro
• [Agda] It is hard to understand the agda error message   mo jia
• [Agda] the recursive definition can not terminate   mo jia
• [Agda] the recursive definition can not terminate   mo jia
• [Agda] Type level computation in inductive types   david.janin at labri.fr
• [Agda] On termination checkers   david.janin at labri.fr
• [Agda] On termination checkers   david.janin at labri.fr
• [Agda] On termination checkers   david.janin at labri.fr
• [Agda] On termination checkers   david.janin at labri.fr
• [Agda] [HoTT] Re: Why do we need judgmental equality?   streicher at mathematik.tu-darmstadt.de
• [Agda] question about termination checker   selinger at mathstat.dal.ca
• [Agda] Small Kernel   selinger at mathstat.dal.ca
• [Agda] installing agda-master with cabal on ubuntu   rick
• [Agda] installing agda-master with cabal on ubuntu   rick
• [Agda] Using Agda in proving computer system correct   mechvel at scico.botik.ru
• [Agda] Raw algebraic structures in the standard library   mechvel at scico.botik.ru
• [Agda] GCD in future standard library   mechvel at scico.botik.ru
• [Agda] GCD in future standard library   mechvel at scico.botik.ru
• [Agda] Raw algebraic structures in the standard library   mechvel at scico.botik.ru
• [Agda] Repository with executable agda code.   mechvel at scico.botik.ru
• [Agda] $ in eq-reasoning   mechvel at scico.botik.ru
• [Agda] $ in eq-reasoning   mechvel at scico.botik.ru
• [Agda] termination checking loop   mechvel at scico.botik.ru
• [Agda] termination checking loop   mechvel at scico.botik.ru
• [Agda] New blog post: Formalize All the Things (in Agda)   mechvel at scico.botik.ru
• [Agda] missed termination failure   mechvel at scico.botik.ru
• [Agda] missed termination failure   mechvel at scico.botik.ru
• [Agda] list comprehensions   mechvel at scico.botik.ru
• [Agda] list comprehensions   mechvel at scico.botik.ru
• [Agda] list comprehensions   mechvel at scico.botik.ru
• [Agda] overlapping _∷_, []   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   mechvel at scico.botik.ru
• [Agda] Question on `unify` function in Reflection API   石尾千晶

Last message date: Tue Dec 31 19:27:06 CET 2019
Archived on: Tue Dec 31 19:27:11 CET 2019

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