2018 Archives by date

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

Starting: Wed Jan 3 19:41:22 CET 2018
Ending: Sun Dec 30 23:01:48 CET 2018
Messages: 826

• [Agda] Bounties for Agda features   Nils Anders Danielsson
• [Agda] 6 Assistant Professor positions at the University of Utrecht   Wouter Swierstra
• [Agda] Show/Solve constraints (C-c C-= and C-c C-s) stopped working   Manny Romero
• [Agda] Show/Solve constraints (C-c C-= and C-c C-s) stopped working   Jesper Cockx
• [Agda] Converting All2 to All   Dr. ERDI Gergo
• [Agda] Converting All2 to All   Dr. ERDI Gergo
• [Agda] Fwd: Converting All2 to All   Matthew Daggitt
• [Agda] Fwd: Converting All2 to All   Dr. ERDI Gergo
• [Agda] Call for Contributions: Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'18)   Anders Mortberg
• [Agda] Fwd: Converting All2 to All   Matthew Daggitt
• [Agda] Instance arguments and types who have a unique construction.   Apostolis Xekoukoulotakis
• [Agda] Instance arguments and types who have a unique construction.   Ulf Norell
• [Agda] Instance arguments and types who have a unique construction.   Apostolis Xekoukoulotakis
• [Agda] Instance arguments and types who have a unique construction.   Ulf Norell
• [Agda] Instance arguments and types who have a unique construction.   Apostolis Xekoukoulotakis
• [Agda] Instance arguments and types who have a unique construction.   Guillaume Brunerie
• [Agda] Instance arguments and types who have a unique construction.   Apostolis Xekoukoulotakis
• [Agda] announce of Binary-3.0   Sergei Meshveliani
• [Agda] ITP abstracts due 25 Jan [Re: Interactive Theorem Proving (ITP) 2018: Second CFP]   Andreas Abel
• [Agda] ICADIWT 2018   edprocess at dline.info
• [Agda] CFP - XXII Brazilian Symposium on Programming Languages   Rodrigo Ribeiro
• [Agda] Infix-notation and TDNR   Frederik Hanghøj Iversen
• [Agda] Infix-notation and TDNR   a.j.rouvoet
• [Agda] Infix-notation and TDNR   Sandro Stucki
• [Agda] proofs for (NON)TERMINATING   Sergei Meshveliani
• [Agda] proofs for (NON)TERMINATING   Nils Anders Danielsson
• [Agda] proofs for (NON)TERMINATING   Jesper Cockx
• [Agda] Is this a recursive record?   Apostolis Xekoukoulotakis
• [Agda] proofs for (NON)TERMINATING   Sergei Meshveliani
• [Agda] Is this a recursive record?   Nils Anders Danielsson
• [Agda] proofs for (NON)TERMINATING   Nils Anders Danielsson
• [Agda] Explicit export   Frederik Hanghøj Iversen
• [Agda] Explicit export   Jesper Cockx
• [Agda] Explicit export   Frederik Hanghøj Iversen
• [Agda] Explicit export   Wolfram Kahl
• [Agda] IO programs examples ?   Serge Leblanc
• [Agda] IO programs examples ?   Guillaume Allais
• [Agda] IO programs examples ?   Sergei Meshveliani
• [Agda] am I doing something fundamentally impredicative in this code? or is there a better approach   Carter Schonwald
• [Agda] am I doing something fundamentally impredicative in this code? or is there a better approach   Carter Schonwald
• [Agda] Binary library reference   Sergei Meshveliani
• [Agda] Binary library reference   Jonathan Prieto-Cubides
• [Agda] Binary library reference   Sergei Meshveliani
• [Agda] Second Call for Papers: PACMPL issue ICFP 2018   Lindsey Kuper
• [Agda] proofs for (NON)TERMINATING   Sergei Meshveliani
• [Agda] proofs for (NON)TERMINATING   Jesper Cockx
• [Agda] proofs for (NON)TERMINATING   Martin Escardo
• [Agda] proofs for (NON)TERMINATING   Sergei Meshveliani
• [Agda] proofs for (NON)TERMINATING   Nils Anders Danielsson
• [Agda] proofs for (NON)TERMINATING   Sergei Meshveliani
• [Agda] Superscript l and r in unicode   Philip Wadler
• [Agda] Superscript l and r in unicode   Dr. ÉRDI Gergő
• [Agda] Superscript l and r in unicode   N. Raghavendra
• [Agda] Superscript l and r in unicode   Philip Wadler
• [Agda] type check with large constant   Sergei Meshveliani
• [Agda] Coinduction and Instance Arguments - is it possible?   Apostolis Xekoukoulotakis
• [Agda] Coinduction and Instance Arguments - is it possible?   Jesper Cockx
• [Agda] Coinduction and Instance Arguments - is it possible?   Apostolis Xekoukoulotakis
• [Agda] type check with large constant   Ulf Norell
• [Agda] type check with large constant   Sergei Meshveliani
• [Agda] type check with large constant   Ulf Norell
• [Agda] Midlands Graduate School 2018   Graham Hutton
• [Agda] C preprocessor with agda   Frederik Hanghøj Iversen
• [Agda] Hoogle for Agda?   Philip Wadler
• [Agda] Hoogle for Agda?   Guillaume Allais
• [Agda] Hoogle for Agda?   Philip Wadler
• [Agda] Hoogle for Agda?   Liam O'Connor
• [Agda] Hoogle for Agda?   John Leo
• [Agda] Hoogle for Agda?   Philip Wadler
• [Agda] Hoogle for Agda?   Philip Wadler
• [Agda] Boolean and Decidable comparison   Philip Wadler
• [Agda] Boolean and Decidable comparison   Miëtek Bak
• [Agda] Boolean and Decidable comparison   Philip Wadler
• [Agda] Boolean and Decidable comparison   Miëtek Bak
• [Agda] Boolean and Decidable comparison   Miëtek Bak
• [Agda] Call for Posters: <Programming> 2018   Sylvia Grewe
• [Agda] Hoogle for Agda?   Liam O'Connor
• [Agda] Finer-grained library control in Agda   Frederik Hanghøj Iversen
• [Agda] Finer-grained library control in Agda   Frederik Hanghøj Iversen
• [Agda] Finer-grained library control in Agda   Ulf Norell
• [Agda] First Call for Papers: 11th ACM SIGPLAN International Conference on Software Language Engineering (SLE 2018)   Andrei Chis
• [Agda] Absolute links in html rendering of Agda files   Martin Escardo
• [Agda] Absolute links in html rendering of Agda files   Guillaume Allais
• [Agda] Hoogle for Agda?   Philip Wadler
• [Agda] Boolean and Decidable comparison   Philip Wadler
• [Agda] Hoogle for Agda?   Andrés Sicard-Ramírez
• [Agda] Boolean and Decidable comparison   Guillaume Allais
• [Agda] Absolute links in html rendering of Agda files   Martin Escardo
• [Agda] Absolute links in html rendering of Agda files   Andreas Abel
• [Agda] Boolean and Decidable comparison   Philip Wadler
• [Agda] Absolute links in html rendering of Agda files   Martín Hötzel Escardó
• [Agda] Some problems with termination checker   v0ιd
• [Agda] Some problems with termination checker   Arseniy Alekseyev
• [Agda] Some problems with termination checker   Guillaume Allais
• [Agda] Call for Contributions: Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'18)   Anders Mortberg
• [Agda] CfP: 4PAD 2018 - 5th International Symposium on Formal Approaches to Parallel and Distributed Systems   Frederic Loulergue
• [Agda] Absolute links in html rendering of Agda files   Andreas Abel
• [Agda] Absolute links in html rendering of Agda files   Martin Escardo
• [Agda] C preprocessor with agda   Nils Anders Danielsson
• [Agda] WiL 2018: Women in Logic Workshop 2nd Call for Papers   Amy Felty
• [Agda] C preprocessor with agda   Frederik Hanghøj Iversen
• [Agda] INLINE-pragma   Frederik Hanghøj Iversen
• [Agda] VerifyThis 2018: Call for Problems and First Announcement   Andrei Paskevich
• [Agda] Proof involving Fin   Peter Thiemann
• [Agda] Proof involving Fin   Bradley Hardy
• [Agda] Proof involving Fin   Peter Thiemann
• [Agda] Serialization to ByteString   Apostolis Xekoukoulotakis
• [Agda] Serialization to ByteString   Ulf Norell
• [Agda] Serialization to ByteString   Apostolis Xekoukoulotakis
• [Agda] Serialization to ByteString   Ulf Norell
• [Agda] List of exports   Frederik Hanghøj Iversen
• [Agda] List of exports   Ulf Norell
• [Agda] Serialization to ByteString   Apostolis Xekoukoulotakis
• [Agda] Serialization to ByteString   Ulf Norell
• [Agda] Serialization to ByteString   Apostolis Xekoukoulotakis
• [Agda] ¬ 0# ? 1#   Sergei Meshveliani
• [Agda] ¬ 0# ? 1#   Sergei Meshveliani
• [Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn   Philip Wadler
• [Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn   Nils Anders Danielsson
• [Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn   Roman
• [Agda] (Semi)RingWithOne   Sergei Meshveliani
• [Agda] (Semi)RingWithOne   Matthew Daggitt
• [Agda] (Semi)RingWithOne   Sergei Meshveliani
• [Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn   Philip Wadler
• [Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn   Roman
• [Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn   Ulf Norell
• [Agda] rewriting before defining   Thorsten Altenkirch
• [Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn   Philip Wadler
• [Agda] List of exports   Frederik Hanghøj Iversen
• [Agda] rewriting before defining   Andreas Abel
• [Agda] rewriting before defining   Thorsten Altenkirch
• [Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn   András Kovács
• [Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn   Philip Wadler
• [Agda] Lists and products   Philip Wadler
• [Agda] Lists and products   Guillaume Allais
• [Agda] Lists and products   Philip Wadler
• [Agda] Mathematically Structured Functional Programming 2018: Call for Papers   Robert Atkey
• [Agda] INLINE-pragma   Frederik Hanghøj Iversen
• [Agda] [Deadline Monday!] TYPES 2018: final call for contributions   Andreas Abel
• [Agda] Mathematically Structured Functional Programming (MSFP 2018) Call for Papers   Shin-Cheng Mu
• [Agda] PARIS workshop @ FLoC 2018 : Programming And Reasoning on Infinite Structures (First CfP)   Andreas Abel
• [Agda] Well-foundedness of list of well-founded elements   How Si Yu
• [Agda] Well-foundedness of list of well-founded elements   Ulf Norell
• [Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn   Philip Wadler
• [Agda] Well-foundedness of list of well-founded elements   How Si Yu
• [Agda] Packaging Agda and compiling it ahead of time   Alex ter Weele
• [Agda] Bug caused by new forcing translation   stvienna wiener
• [Agda] Bug caused by new forcing translation   Ulf Norell
• [Agda] Packaging Agda and compiling it ahead of time   James Wood
• [Agda] rewriting before defining   Jesper Cockx
• [Agda] rewriting before defining   Thorsten Altenkirch
• [Agda] INLINE-pragma   Nils Anders Danielsson
• [Agda] VerifyThis 2018: Call for Participation and Travel Grants   Andrei Paskevich
• [Agda] Feedback on upcoming version of the standard library   Matthew Daggitt
• [Agda] debugPrint : Does it work correctly?   Apostolis Xekoukoulotakis
• [Agda] Checking the types of terms   Philip Wadler
• [Agda] Checking the types of terms   Larrytheliquid
• [Agda] debugPrint : Does it work correctly?   Ulf Norell
• [Agda] debugPrint : Does it work correctly?   Apostolis Xekoukoulotakis
• [Agda] Checking the types of terms   Philip Wadler
• [Agda] Checking the types of terms   Guillaume Brunerie
• [Agda] Checking the types of terms   Philip Wadler
• [Agda] debugPrint : Does it work correctly?   Ulf Norell
• [Agda] LFMTP'18: Logical Frameworks and Meta Languages: Theory and Practice - Call for Papers   Frédéric Blanqui
• [Agda] Checking the types of terms   Nils Anders Danielsson
• [Agda] LFMTP - call for papers   Ana Bove
• [Agda] coinductively defined families   Thorsten Altenkirch
• [Agda] coinductively defined families   Jesper Cockx
• [Agda] 1st call for papers: Trends in Functional Programming, 11-13 june 2018, Chalmers Campus Johanneberg, Gothenburg   Peter Achten
• [Agda] coinductively defined families   Jesper Cockx
• [Agda] coinductively defined families   Andreas Abel
• [Agda] coinductively defined families   Thorsten Altenkirch
• [Agda] Partiality/delay monad [was: proofs for (NON)TERMINATING]   Sandro Stucki
• [Agda] coinductively defined families   Henning Basold
• [Agda] Partiality/delay monad [was: proofs for (NON)TERMINATING]   Nils Anders Danielsson
• [Agda] Partiality/delay monad [was: proofs for (NON)TERMINATING]   Guillaume Allais
• [Agda] coinductively defined families   Thorsten Altenkirch
• [Agda] Final Call for Papers: PACMPL issue ICFP 2018   Lindsey Kuper
• [Agda] module _{a b}   Sergei Meshveliani
• [Agda] module _{a b}   Matthew Daggitt
• [Agda] Midlands Graduate School 2018 - final call for participation   Graham Hutton
• [Agda] [ANNOUNCE] Standard library 0.15   Matthew Daggitt
• [Agda] 1st CfP: IFL 2018 (30th Symposium on Implementation and Application of Functional Languages)   Jurriaan Hage
• [Agda] +-*- swap in library   Sergei Meshveliani
• [Agda] Call for Participation: <Programming> 2018 in Nice   Sylvia Grewe
• [Agda] +-*- swap in library   Matthew Daggitt
• [Agda] Federated Logic Conference student travel support   Jeremy Avigad
• [Agda] Tenure track Assistant Professor in Computer Science directed towards Logic of Programs (Deadline: April 3)   Erik Palmgren
• [Agda] Cannot unquote non-canonical type checking computation   Apostolis Xekoukoulotakis
• [Agda] Cannot unquote non-canonical type checking computation   Ulf Norell
• [Agda] FoPPS Logic and Learning School (Oxford, July 1-6)   Andrzej Murawski
• [Agda] Cannot unquote non-canonical type checking computation   Apostolis Xekoukoulotakis
• [Agda] Bug in simplification?   Philip Wadler
• [Agda] Bug in simplification?   András Kovács
• [Agda] Bug in simplification?   Philip Wadler
• [Agda] Bug in simplification?   Ulf Norell
• [Agda] Confused about rewriting   Philip Wadler
• [Agda] Posts in security in Swansea (possibly connected to Agda) deadline Fri 22/3/18   Setzer A.G.
• [Agda] Call for Tutorial Proposals: ICFP 2018   Lindsey Kuper
• [Agda] Confused about rewriting   Ulf Norell
• [Agda] Confused about rewriting   Philip Wadler
• [Agda] Bug in simplification?   Philip Wadler
• [Agda] Syntax declarations   Philip Wadler
• [Agda] Syntax declarations   Adam Sandberg Eriksson
• [Agda] Syntax declarations   Philip Wadler
• [Agda] Syntax declarations   Ulf Norell
• [Agda] Syntax declarations   Andreas Abel
• [Agda] Midlands Graduate School - extended registration deadline   Graham Hutton
• [Agda] Partiality/delay monad   Nils Anders Danielsson
• [Agda] Confused about rewriting   Nils Anders Danielsson
• [Agda] Syntax declarations   Philip Wadler
• [Agda] Partiality/delay monad   Guillaume Allais
• [Agda] Syntax declarations   Ulf Norell
• [Agda] Confused about rewriting   Philip Wadler
• [Agda] Syntax declarations   Philip Wadler
• [Agda] Partiality/delay monad   Nils Anders Danielsson
• [Agda] nullary copattern matching   Christian Sattler
• [Agda] nullary copattern matching   Andreas Abel
• [Agda] Syntax declarations   Ulf Norell
• [Agda] nullary copattern matching   Thorsten Altenkirch
• [Agda] Syntax declarations   Philip Wadler
• [Agda] Right Distributivity   Philip Wadler
• [Agda] Right Distributivity   Nils Anders Danielsson
• [Agda] Right Distributivity   Philip Wadler
• [Agda] Right Distributivity   Matthew Daggitt
• [Agda] Right Distributivity   Philip Wadler
• [Agda] `Pointwise' over Setoid   Sergei Meshveliani
• [Agda] `Pointwise' over Setoid   Matthew Daggitt
• [Agda] Is bottom initial without functional extensionality?   Dan Krejsa
• [Agda] Is bottom initial without functional extensionality?   Jesper Cockx
• [Agda] Instance resolution question   Apostolis Xekoukoulotakis
• [Agda] Instance resolution question   Ulf Norell
• [Agda] Instance resolution question   Apostolis Xekoukoulotakis
• [Agda] Instance resolution question   Ulf Norell
• [Agda] Instance resolution question   Apostolis Xekoukoulotakis
• [Agda] strictness place   Sergei Meshveliani
• [Agda] strictness place   Nils Anders Danielsson
• [Agda] strictness place   Ulf Norell
• [Agda] strictness place   Philipp Hausmann
• [Agda] literature on Coq page   Sergei Meshveliani
• [Agda] strictness place   Wolfram Kahl
• [Agda] Confusion about rewrite mechanism   VinaLx
• [Agda] SBLP 2018 second call for papers   Carlos Camarao
• [Agda] new generalize feature, first version   Peter Divianszky
• [Agda] Operational and Denotational, Typed and Untyped Lambda Calculus   Philip Wadler
• [Agda] Operational and Denotational, Typed and Untyped Lambda Calculus   Nils Anders Danielsson
• [Agda] new generalize feature, first version   Nils Anders Danielsson
• [Agda] new generalize feature, first version   Martin Escardo
• [Agda] new generalize feature, first version   Thorsten Altenkirch
• [Agda] new generalize feature, first version   Robby Findler
• [Agda] new generalize feature, first version   Apostolis Xekoukoulotakis
• [Agda] new generalize feature, first version   Peter Divianszky
• [Agda] new generalize feature, first version   Peter Divianszky
• [Agda] new generalize feature, first version   Joachim Breitner
• [Agda] new generalize feature, first version   Jannis Limperg
• [Agda] new generalize feature, first version   Nils Anders Danielsson
• [Agda] new generalize feature, first version   Nils Anders Danielsson
• [Agda] Operational and Denotational, Typed and Untyped Lambda Calculus   Philip Wadler
• [Agda] Operational and Denotational, Typed and Untyped Lambda Calculus   Larrytheliquid
• [Agda] Operational and Denotational, Typed and Untyped Lambda Calculus   Martin Escardo
• [Agda] new generalize feature, first version   Peter Divianszky
• [Agda] new generalize feature, first version   Nils Anders Danielsson
• [Agda] new generalize feature, first version   Peter Divianszky
• [Agda] new generalize feature, first version   Peter Divianszky
• [Agda] new generalize feature, first version   Nils Anders Danielsson
• [Agda] new generalize feature, first version   Arseniy Alekseyev
• [Agda] Checking the types of terms   Peter Hancock
• [Agda] new generalize feature, first version   Peter Divianszky
• [Agda] Mathematically Structured Functional Programming 2018: Final Call for Papers   Robert Atkey
• [Agda] new generalize feature, first version   Peter Divianszky
• [Agda] new generalize feature, first version   Nils Anders Danielsson
• [Agda] new generalize feature, first version   Martin Stone Davis
• [Agda] new generalize feature, first version   Andrés Sicard-Ramírez
• [Agda] new generalize feature, first version   Peter Divianszky
• [Agda] new generalize feature, first version   Peter Divianszky
• [Agda] new generalize feature, first version   Nils Anders Danielsson
• [Agda] new generalize feature, first version   Martin Stone Davis
• [Agda] new generalize feature, first version   Peter Divianszky
• [Agda] 2nd CfP: IFL 2018 (30th Symposium on Implementation and Application of Functional Languages)   Jurriaan Hage
• [Agda] Operational and Denotational, Typed and Untyped Lambda Calculus   Philip Wadler
• [Agda] Encoding higher lambda calculus in agda   How Si Yu
• [Agda] Encoding higher lambda calculus in agda   Jason -Zhong Sheng- Hu
• [Agda] Encoding higher lambda calculus in agda   András Kovács
• [Agda] Encoding higher lambda calculus in agda   Henning Basold
• [Agda] Encoding higher lambda calculus in agda   How Si Yu
• [Agda] Autumn school "Proof and Computation"   Chuangjie Xu
• [Agda] Final Call for Contributions: Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'18)   Anders Mortberg
• [Agda] Phd/PostDoc position on linear types and session types   Peter Thiemann
• [Agda] ANN: "Evolution of a type-checker" & "Dependently-typed programming"   Pierre-Evariste Dagand
• [Agda] AIM XXVII - Göteborg, 4 – 9 June 2018   Jesper Cockx
• [Agda] AIM XXVII - Göteborg, 4 – 9 June 2018   Jesper Cockx
• [Agda] AIM XXVII - Göteborg, 4 – 9 June 2018   Nils Anders Danielsson
• [Agda] LFMTP'18 deadline extension   Ana Bove
• [Agda] SBLP 2018 last call for papers   Carlos Camarao
• [Agda] 2nd call for papers: Trends in Functional Programming, 11-13 june 2018, Chalmers Campus Johanneberg, Gothenburg   Peter Achten
• [Agda] Call for Participation: AFP Summer School in Utrecht   Swierstra, W.S. (Wouter)
• [Agda] type of []   Sergei Meshveliani
• [Agda] type of []   Thorsten Altenkirch
• [Agda] type of []   Sergei Meshveliani
• [Agda] Infix in Modules with Parameters   Philip Wadler
• [Agda] Infix in Modules with Parameters   Martin Stone Davis
• [Agda] Infix in Modules with Parameters   Philip Wadler
• [Agda] Infix in Modules with Parameters   Dr. ERDI Gergo
• [Agda] Infix in Modules with Parameters   Jacques Carette
• [Agda] Infix in Modules with Parameters   Guillaume Allais
• [Agda] ASN.1 and type theory   David Wahlstedt
• [Agda] ASN.1 and type theory   Nils Anders Danielsson
• [Agda] SBLP 2018 deadline extension   Carlos Camarao
• [Agda] ASN.1 and type theory   David Wahlstedt
• [Agda] Redundant imports   Martín Hötzel Escardó
• [Agda] Redundant imports   Nils Anders Danielsson
• [Agda] Redundant imports   Sergei Meshveliani
• [Agda] Redundant imports   Guillaume Allais
• [Agda] Redundant imports   Martin Escardo
• [Agda] Redundant imports   Guillaume Allais
• [Agda] Redundant imports   Martin Escardo
• [Agda] Allow cyclic module imports   Martín Hötzel Escardó
• [Agda] agda-mode input method   Frederik Hanghøj Iversen
• [Agda] Allow cyclic module imports   Nils Anders Danielsson
• [Agda] agda-mode input method   Nils Anders Danielsson
• [Agda] Allow cyclic module imports   Martin Escardo
• [Agda] agda-mode input method   Frederik Hanghøj Iversen
• [Agda] Allow cyclic module imports   Sergei Meshveliani
• [Agda] agda-mode input method   Sandro Stucki
• [Agda] agda-mode input method   John Leo
• [Agda] agda-mode input method   Nils Anders Danielsson
• [Agda] agda-mode input method   Frederik Hanghøj Iversen
• [Agda] Allow cyclic module imports   Nils Anders Danielsson
• [Agda] agda-mode input method   Nils Anders Danielsson
• [Agda] Allow cyclic module imports   Tom Murphy
• [Agda] Journal of Functional Programming - Call for PhD Abstracts   Graham Hutton
• [Agda] final call for papers: Trends in Functional Programming, 11-13 june 2018, Chalmers Campus Johanneberg, Gothenburg - deadline extended -   Peter Achten
• [Agda] how to set level   Sergei Meshveliani
• [Agda] 3rd CfP: IFL 2018 (30th Symposium on Implementation and Application of Functional Languages)   Jurriaan Hage
• [Agda] how to set level   Sergei Meshveliani
• [Agda] how to set level   Sergei Meshveliani
• [Agda] strange "Unreachable clause"   Sergei Meshveliani
• [Agda] strange "Unreachable clause"   James Wood
• [Agda] strange "Unreachable clause"   Ulf Norell
• [Agda] Trends in Functional Programming: deadline for extended abstracts extended   Andreas Abel
• [Agda] strange "Unreachable clause"   Sergei Meshveliani
• [Agda] AIM XXVII - Göteborg, 4 – 9 June 2018   Jesper Cockx
• [Agda] Symmetry   Philip Wadler
• [Agda] Symmetry   James Wood
• [Agda] Blog post: The Agda's New Sorts   Jesper Cockx
• [Agda] Symmetry   Philip Wadler
• [Agda] Symmetry   Jacques Carette
• [Agda] Symmetry   Philip Wadler
• [Agda] How does one debug a programme that one has proved correct?   Philip Wadler
• [Agda] How does one debug a programme that one has proved correct?   Ulf Norell
• [Agda] How does one debug a programme that one has proved correct?   Philip Wadler
• [Agda] How does one debug a programme that one has proved correct?   Ulf Norell
• [Agda] Bishop's work on Type Theory   Martin Escardo
• [Agda] How does one debug a programme that one has proved correct?   Philip Wadler
• [Agda] How does one debug a programme that one has proved correct?   Ulf Norell
• [Agda] How does one debug a programme that one has proved correct?   Philip Wadler
• [Agda] How does one debug a programme that one has proved correct?   Philip Wadler
• [Agda] Numerical Methods in Functional Programming (CfP)   dominic at steinitz.org
• [Agda] Blog post: The Agda's New Sorts   Thorsten Altenkirch
• [Agda] Blog post: The Agda's New Sorts   Martin Escardo
• [Agda] How does one debug a programme that one has proved correct?   Philip Wadler
• [Agda] The joys and sorrows of abstraction   Philip Wadler
• [Agda] The joys and sorrows of abstraction   Wolfram Kahl
• [Agda] The joys and sorrows of abstraction   Nils Anders Danielsson
• [Agda] Blog post: The Agda's New Sorts   Henning Basold
• [Agda] How does one debug a programme that one has proved correct?   Ulf Norell
• [Agda] How does one debug a programme that one has proved correct?   Philip Wadler
• [Agda] The joys and sorrows of abstraction   Philip Wadler
• [Agda] Blog post: The Agda's New Sorts   Jon Sterling
• [Agda] The joys and sorrows of abstraction   Nils Anders Danielsson
• [Agda] The joys and sorrows of abstraction   Philip Wadler
• [Agda] The joys and sorrows of abstraction   Martin Escardo
• [Agda] The joys and sorrows of abstraction   Philip Wadler
• [Agda] The joys and sorrows of abstraction   Ulf Norell
• [Agda] The joys and sorrows of abstraction   Martin Escardo
• [Agda] The joys and sorrows of abstraction   Apostolis Xekoukoulotakis
• [Agda] The joys and sorrows of abstraction   Philip Wadler
• [Agda] The joys and sorrows of abstraction   Martin Escardo
• [Agda] the joys and sorrows of abstraction.   Peter Hancock
• [Agda] The joys and sorrows of abstraction   Martin Escardo
• [Agda] the joys and sorrows of abstraction.   Martin Escardo
• [Agda] The joys and sorrows of abstraction   Arseniy Alekseyev
• [Agda] The joys and sorrows of abstraction   Arseniy Alekseyev
• [Agda] the joys and sorrows of abstraction.   Matthieu Sozeau
• [Agda] The joys and sorrows of abstraction   Andrew Pitts
• [Agda] Foundations of copatterns [Re: The joys and sorrows of abstraction]   Andreas Abel
• [Agda] The joys and sorrows of abstraction   Jesper Cockx
• [Agda] The joys and sorrows of abstraction   Martin Escardo
• [Agda] Blog post: The Agda's New Sorts   Jesper Cockx
• [Agda] Blog post: The Agda's New Sorts   Philip Wadler
• [Agda] Blog post: The Agda's New Sorts   Jon Sterling
• [Agda] new generalize feature, first version   Jesper Cockx
• [Agda] New deadline for paper submission to SBLP 2018   Carlos Camarao
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Andrés Sicard-Ramírez
• [Agda] Formal Methods internship at Arm Research   Dominic Mulligan
• [Agda] Autumn school "Proof and Computation"   Chuangjie Xu
• [Agda] new generalize feature, first version   Peter Divianszky
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Sergei Meshveliani
• [Agda] Pretty Print Line Length   Philip Wadler
• [Agda] Pretty Print Line Length   Ulf Norell
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Nils Anders Danielsson
• [Agda] Pretty Print Line Length   Philip Wadler
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Ulf Norell
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Ulf Norell
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Nils Anders Danielsson
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Jesper Cockx
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Sergei Meshveliani
• [Agda] "unsolved metas" in candidate   Sergei Meshveliani
• [Agda] "unsolved metas" in candidate   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Ulf Norell
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Andrés Sicard-Ramírez
• [Agda] implicit/explicit difference in candidate   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Arseniy Alekseyev
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 2   Andrés Sicard-Ramírez
• [Agda] implicit/explicit difference in candidate   Andrés Sicard-Ramírez
• [Agda] implicit/explicit difference in candidate   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Ulf Norell
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1   Arseniy Alekseyev
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 2   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 2   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.4 release candidate 2   Nils Anders Danielsson
• [Agda] Second Call for Papers: 11th ACM SIGPLAN International Conference on Software Language Engineering (SLE 2018)   Andrei Chis
• [Agda] [ANNOUNCE] Agda 2.5.4   Andrés Sicard-Ramírez
• [Agda] Mathematically Structured Functional Programming 2018: Call for Participation   Robert Atkey
• [Agda] Final Call for Presentations HOPE 2018   Filip Sieczkowski
• [Agda] type check performance   Sergei Meshveliani
• [Agda] TLA+ or LTL in agda ?   Apostolis Xekoukoulotakis
• [Agda] TLA+ or LTL in agda ?   Ulf Norell
• [Agda] type check performance   Jesper Louis Andersen
• [Agda] type check performance   Sergei Meshveliani
• [Agda] TLA+ or LTL in agda ?   Setzer A.G.
• [Agda] Standard library 0.16   Matthew Daggitt
• [Agda] type check performance   Martin Escardo
• [Agda] type check performance   Nils Anders Danielsson
• [Agda] type check performance   Martin Escardo
• [Agda] Multitheading Agda?   Jason -Zhong Sheng- Hu
• [Agda] HOPE 2018: Deadline extension until June 15th   Filip Sieczkowski
• [Agda] Multitheading Agda?   Nils Anders Danielsson
• [Agda] Call for draft papers for presentation at IFL 2018 (Implementation and Application of Functional Languages)   Jurriaan Hage
• [Agda] Announcement: MPC 2019, Porto, Portugal   Graham Hutton
• [Agda] Call for Conference Grant Applications (Inclusiveness Target Countries)   Ambrus Kaposi
• [Agda] Fwd: [Eutypes] Call for STSMs, deadline July 1, 2018   Andreas Abel
• [Agda] type:type locally?   Thorsten Altenkirch
• [Agda] Typed Jigger in vanilla Agda.   Roman
• [Agda] Emacs mode subscripts and superscripts   Philip Wadler
• [Agda] Emacs mode subscripts and superscripts   Guillaume Allais
• [Agda] Typed Jigger in vanilla Agda.   Guillaume Allais
• [Agda] Typed Jigger in vanilla Agda.   Roman
• [Agda] type:type locally?   Jesper Cockx
• [Agda] type:type locally?   Jesper Cockx
• [Agda] libraries for Bin   Sergei Meshveliani
• [Agda] libraries for Bin   Martin Escardo
• [Agda] PhD/Postdoc vacancy: Homotopy type theory and probabilistic programming   Bas Spitters
• [Agda] libraries for Bin   Sergei Meshveliani
• [Agda] libraries for Bin   Anton Trunov
• [Agda] libraries for Bin   Arseniy Alekseyev
• [Agda] unsolved meta with abstraction example   rick
• [Agda] unsolved meta with abstraction example   Ulf Norell
• [Agda] libraries for Bin   Sergei Meshveliani
• [Agda] Formalization of Agda's universe polymorphism   Stefan Monnier
• [Agda] Literate Agda bit rot   Philip Wadler
• [Agda] libraries for Bin   Anton Trunov
• [Agda] unification using more complex with abstractions   rick
• [Agda] unification using more complex with abstractions   Jason -Zhong Sheng- Hu
• [Agda] Formalization of Agda's universe polymorphism   Jesper Cockx
• [Agda] Formalization of Agda's universe polymorphism   Roman
• [Agda] libraries for Bin   Sergei Meshveliani
• [Agda] libraries for Bin   Anton Trunov
• [Agda] unification using more complex with abstractions   rick
• [Agda] unification using more complex with abstractions   Jason -Zhong Sheng- Hu
• [Agda] Progress + Preservation = Evaluation   Philip Wadler
• [Agda] [TYPES] Progress + Preservation = Evaluation   William J. Bowman
• [Agda] Progress + Preservation = Evaluation   Philip Wadler
• [Agda] [TYPES] Progress + Preservation = Evaluation   Pierre Courtieu
• [Agda] [TYPES] Progress + Preservation = Evaluation   Eelco Visser
• [Agda] [TYPES] Progress + Preservation = Evaluation   Eelco Visser
• [Agda] [TYPES] Progress + Preservation = Evaluation   Philip Wadler
• [Agda] [TYPES] Progress + Preservation = Evaluation   Sam Lindley
• [Agda] [TYPES] Progress + Preservation = Evaluation   Andreas Abel
• [Agda] [TYPES] Progress + Preservation = Evaluation   Philip Wadler
• [Agda] [TYPES] Progress + Preservation = Evaluation   Roman
• [Agda] Post-proceedings TYPES'18: call for papers   José Carlos Espírito Santo
• [Agda] cong with wildcard   Sergei Meshveliani
• [Agda] cong with wildcard   Arseniy Alekseyev
• [Agda] cong with wildcard   Matthew Daggitt
• [Agda] LAST CALL for draft papers for presentation at IFL 2018 (deadline this week)   Jurriaan Hage
• [Agda] [TYPES] Progress + Preservation = Evaluation   Oleg
• [Agda] unification using more complex with abstractions   rick
• [Agda] [TYPES] Progress + Preservation = Evaluation   Philip Wadler
• [Agda] Why does this pass the positivity checker?   Neel Krishnaswami
• [Agda] [ANNOUNCE] Agda 2.5.4.1   Andrés Sicard-Ramírez
• [Agda] Why does this pass the positivity checker?   Jesper Cockx
• [Agda] Why does this pass the positivity checker?   Neel Krishnaswami
• [Agda] Why does this pass the positivity checker?   Jesper Cockx
• [Agda] Why does this pass the positivity checker?   Thorsten Altenkirch
• [Agda] Reflection with terms in different universes   Jannis Limperg
• [Agda] Newbie question: For nonnegative rationals ‘a’ and ‘b’, how to prove ‘a - b’ is nonnegative, given that ‘b ≤ a’?   Zambonifofex
• [Agda] Reflection with terms in different universes   Roman
• [Agda] Reflection with terms in different universes   Roman
• [Agda] Reflection with terms in different universes   Jannis Limperg
• [Agda] CPP 2019: Call for Papers   Magnus Myreen
• [Agda] Generating pretty HTML listings of Agda repos using travis and jlimperg/agda-stdlib   Andreas Abel
• [Agda] Two PhD Positions in Program Verification   Amin Timany
• [Agda] redefining a value for `with'   Sergei Meshveliani
• [Agda] Checking termination is not sufficiently exploratory.   Serge Leblanc
• [Agda] Checking termination is not sufficiently exploratory.   a.j.rouvoet
• [Agda] Checking termination is not sufficiently exploratory.   Serge Leblanc
• [Agda] Checking termination is not sufficiently exploratory.   a.j.rouvoet
• [Agda] [TYPES] Progress + Preservation = Evaluation   Nils Anders Danielsson
• [Agda] Checking termination is not sufficiently exploratory.   Serge Leblanc
• [Agda] Checking termination is not sufficiently exploratory.   Jason -Zhong Sheng- Hu
• [Agda] Checking termination is not sufficiently exploratory.   Serge Leblanc
• [Agda] Checking termination is not sufficiently exploratory.   Robbert Krebbers
• [Agda] [TYPES] Progress + Preservation = Evaluation   Philip Wadler
• [Agda] more unification using more complex with abstractions   rick
• [Agda] more unification using more complex with abstractions   rick
• [Agda] Checking termination is not sufficiently exploratory.   Serge Leblanc
• [Agda] Newbie question: For nonnegative rationals ‘a’ and ‘b’, how to prove ‘a - b’ is nonnegative, given that ‘b ≤ a’?   Matthew Daggitt
• [Agda] Checking termination is not sufficiently exploratory.   Serge Leblanc
• [Agda] more unification using more complex with abstractions   Nils Anders Danielsson
• [Agda] vs++[]==vs for vectors   Kenichi Asai
• [Agda] vs++[]==vs for vectors   Roman
• [Agda] Checking termination is not sufficiently exploratory.   Guillaume Allais
• [Agda] WellFounded usage   Sergei Meshveliani
• [Agda] Checking termination is not sufficiently exploratory.   Serge Leblanc
• [Agda] Checking termination is not sufficiently exploratory.   Guillaume Allais
• [Agda] WellFounded usage   Sergei Meshveliani
• [Agda] Odd behaviour of Agda   Philip Wadler
• [Agda] Odd behaviour of Agda   Guillaume Allais
• [Agda] Odd behaviour of Agda   Sergei Meshveliani
• [Agda] Checking termination is not sufficiently exploratory.   Serge Leblanc
• [Agda] Standard WellFounded   Sergei Meshveliani
• [Agda] Call for Participation: ICFP 2018   Lindsey Kuper
• [Agda] Checking termination is not sufficiently exploratory.   Guillaume Allais
• [Agda] Odd behaviour of Agda   Philip Wadler
• [Agda] Standard WellFounded   Sergei Meshveliani
• [Agda] Standard WellFounded   Sandro Stucki
• [Agda] Standard WellFounded   Sergei Meshveliani
• [Agda] Standard WellFounded   Sergei Meshveliani
• [Agda] Standard WellFounded   Sergei Meshveliani
• [Agda] Standard WellFounded   Arseniy Alekseyev
• [Agda] Standard WellFounded   Sergei Meshveliani
• [Agda] Standard WellFounded   Sergei Meshveliani
• [Agda] Standard WellFounded   Arseniy Alekseyev
• [Agda] Standard WellFounded   Arseniy Alekseyev
• [Agda] Standard WellFounded   Sergei Meshveliani
• [Agda] Checking termination is not sufficiently exploratory.   Andreas Abel
• [Agda] First Call for Participation for IFL 2018 (Implementation and Application of Functional Languages)   Jurriaan Hage
• [Agda] AIM XXVIII - Nottingham, October 15-20   Nicolai Kraus
• [Agda] PhD thesis position on formal proofs and programming languages at Siemens Mobility, France   Danko Ilik
• [Agda] Standard library 0.16.1   Matthew Daggitt
• [Agda] New assistant/associate professor positions in Nottingham   Graham Hutton
• [Agda] proposal with WellFounded   Sergei Meshveliani
• [Agda] proposal with WellFounded   Sergei Meshveliani
• [Agda] proposal with WellFounded   Ulf Norell
• [Agda] Call for Conference Grant Applications (Inclusiveness Target Countries)   Ambrus Kaposi
• [Agda] 8,9 Oct: EUTypes meeting in Aarhus   Bas Spitters
• [Agda] Positions at Nottingham   Thorsten Altenkirch
• [Agda] Binary-4 announcement   Sergei Meshveliani
• [Agda] `accessible' for ℕ   Sergei Meshveliani
• [Agda] `accessible' for ℕ   Ulf Norell
• [Agda] `accessible' for ℕ   Sergei Meshveliani
• [Agda] Mathematics of Program Construction (MPC), Portugal, 2019   Graham Hutton
• [Agda] Type mismatch? Tipo miskongruas?   Serge Leblanc
• [Agda] Type mismatch? Tipo miskongruas?   Jason -Zhong Sheng- Hu
• [Agda] Type mismatch? Tipo miskongruas?   Jesper Cockx
• [Agda] Type mismatch? Tipo miskongruas?   Nils Anders Danielsson
• [Agda] Literate Agda bit rot   Nils Anders Danielsson
• [Agda] Agda Implementors' Meeting XXVIII - Nottingham, October 15-20   Nicolai Kraus
• [Agda] announcing Cedille 1.0.0   Aaron Stump
• [Agda] using (Acc _<_)   Sergei Meshveliani
• [Agda] CPP 2019: Final Call for Papers   Magnus Myreen
• [Agda] import behavior   Sergei Meshveliani
• [Agda] import behavior   Matthew Daggitt
• [Agda] import behavior   Matthew Daggitt
• [Agda] Mechanized semantics of constraint/logic programming languages   a.j.rouvoet
• [Agda] Mechanized semantics of constraint/logic programming languages   Bas Spitters
• [Agda] Mechanized semantics of constraint/logic programming languages   Gabriel Scherer
• [Agda] Bug report   Philip Wadler
• [Agda] Bug report   Philip Wadler
• [Agda] Bug report   Guillaume Allais
• [Agda] New blog post: Elaborating dependent (co)pattern matching   Jesper Cockx
• [Agda] two questions on type checker   Sergei Meshveliani
• [Agda] two questions on type checker   Jason -Zhong Sheng- Hu
• [Agda] two questions on type checker   Guillaume Allais
• [Agda] a version for Fin   Sergei Meshveliani
• [Agda] Position of let statements and eager evaluation.   Apostolis Xekoukoulotakis
• [Agda] Proving properties about a datatype with a functional component   Shin-Cheng Mu
• [Agda] Proving properties about a datatype with a functional component   Andrea Vezzosi
• [Agda] Proving properties about a datatype with a functional component   Martin Escardo
• [Agda] Offer of Elisp help   David Thrane Christiansen
• [Agda] Issue with sized types (max of two sizes less than i)   Guillaume Brunerie
• [Agda] Offer of Elisp help   Alan & Kim Zimmerman
• [Agda] Offer of Elisp help   Thorsten Altenkirch
• [Agda] Issue with sized types (max of two sizes less than i)   Nils Anders Danielsson
• [Agda] Agda Compiler Alterations Guide   Musa Al-hassy
• [Agda] Agda Compiler Alterations Guide   Jesper Cockx
• [Agda] Agda Compiler Alterations Guide   Musa Al-hassy
• [Agda] Questions about logic   Silvio Frischknecht
• [Agda] Questions about logic   Henning Basold
• [Agda] Questions about logic   Ambrus Kaposi
• [Agda] Questions about logic   Jesper Cockx
• [Agda] Questions about logic   Peter Hancock
• [Agda] Questions about logic   Thorsten Altenkirch
• [Agda] Questions about logic   Sergei Meshveliani
• [Agda] Questions about logic   Jesper Cockx
• [Agda] Questions about logic   Sergei Meshveliani
• [Agda] Questions about logic   Thorsten Altenkirch
• [Agda] Questions about logic   Silvio Frischknecht
• [Agda] [ Agda-Pkg ] The package manager   Jonathan Steven Prieto Cubides
• [Agda] Impredicativity   Simon Boulier
• [Agda] Impredicativity   Jesper Cockx
• [Agda] Impredicativity   Simon Boulier
• [Agda] Impredicativity   Martin Escardo
• [Agda] Certain Emacs commands not working; being reported as "undefined"   Dave Martin
• [Agda] Certain Emacs commands not working; being reported as "undefined"   Benjamin Price
• [Agda] Certain Emacs commands not working; being reported as "undefined"   Jason -Zhong Sheng- Hu
• [Agda] Participation in Google Summer of Code   Marko Dimjašević
• [Agda] Standard library 0.17   Matthew Daggitt
• [Agda] Certain Emacs commands not working; being reported as "undefined"   Andrea Vezzosi
• [Agda] Offer of Elisp help   Peter Divianszky
• [Agda] Initial Algebra Semantics for Lambda Calculus   Martín
• [Agda] Initial Algebra Semantics for Lambda Calculus   Neil Ghani
• [Agda] Disable post projections?   Martin Escardo
• [Agda] Offer of Elisp help   Thorsten Altenkirch
• [Agda] Offer of Elisp help   Apostolis Xekoukoulotakis
• [Agda] Offer of Elisp help   Bas Spitters
• [Agda] Offer of Elisp help   Philip Wadler
• [Agda] Offer of Elisp help   Apostolis Xekoukoulotakis
• [Agda] Offer of Elisp help   Philip Wadler
• [Agda] Offer of Elisp help   Simon Huber
• [Agda] Offer of Elisp help   Nils Anders Danielsson
• [Agda] Equalities between elements of different sizes   Guillaume Brunerie
• [Agda] Equalities between elements of different sizes   Oleg Grenrus
• [Agda] Equalities between elements of different sizes   Guillaume Brunerie
• [Agda] ETAPS 2019 2nd joint call for papers   Tarmo Uustalu
• [Agda] MirageOS unikernels written in Agda.   Apostolis Xekoukoulotakis
• [Agda] What style of proof irrelevance do you prefer: annotated or inferred?   Jesper Cockx
• [Agda] Installing Idris without breaking Agda   Dave Martin
• [Agda] Installing Idris without breaking Agda   Tom Murphy
• [Agda] What style of proof irrelevance do you prefer: annotated or inferred?   Jon Sterling
• [Agda] What style of proof irrelevance do you prefer: annotated or inferred?   Apostolis Xekoukoulotakis
• [Agda] Installing Idris without breaking Agda   Dave Martin
• [Agda] Installing Idris without breaking Agda   Dave Martin
• [Agda] Installing Idris without breaking Agda   mukesh tiwari
• [Agda] Installing Idris without breaking Agda   Dave Martin
• [Agda] Installing Idris without breaking Agda   Apostolis Xekoukoulotakis
• [Agda] Installing Idris without breaking Agda   András Kovács
• [Agda] Installing Idris without breaking Agda   Dave Martin
• [Agda] Installing Idris without breaking Agda   Dave Martin
• [Agda] Installing Idris without breaking Agda   András Kovács
• [Agda] Installing Idris without breaking Agda   Dave Martin
• [Agda] Installing Idris without breaking Agda   András Kovács
• [Agda] Installing Idris without breaking Agda   mukesh tiwari
• [Agda] Installing Idris without breaking Agda   Dave Martin
• [Agda] What style of proof irrelevance do you prefer: annotated or inferred?   Jesper Cockx
• [Agda] What style of proof irrelevance do you prefer: annotated or inferred?   Andreas Nuyts
• [Agda] [ANNOUNCE] Agda 2.5.4.2   Andres Sicard Ramirez
• [Agda] Call For Workshop Proposals   Sam Tobin-Hochstadt
• [Agda] [ANNOUNCE] Agda 2.5.4.2   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.4.2   Matthew Daggitt
• [Agda] [ANNOUNCE] Agda 2.5.4.2   Andres Sicard Ramirez
• [Agda] Disable post projections?   Miëtek Bak
• [Agda] Disable post projections?   Jesper Cockx
• [Agda] Disable post projections?   Martin Escardo
• [Agda] Disable post projections?   Guillaume Brunerie
• [Agda] Equalities between elements of different sizes   Guillaume Allais
• [Agda] Installing Idris without breaking Agda   Nils Anders Danielsson
• [Agda] Disable post projections?   Jesper Cockx
• [Agda] Journal of Functional Programming - Call for PhD Abstracts   Graham Hutton
• [Agda] Fwd: Journal of Functional Programming - Call for PhD Abstracts   Andreas Abel
• [Agda] agda-ocaml - experimental backend   Apostolis Xekoukoulotakis
• [Agda] lib for Development Agda   Sergei Meshveliani
• [Agda] lib for Development Agda   Matthew Daggitt
• [Agda] lib for Development Agda   Guillaume Allais
• [Agda] parasitic arguments in equality proofs   Sergei Meshveliani
• [Agda] overloading operations   Sergei Meshveliani
• [Agda] I want implicit coercions in Agda   Martin Escardo
• [Agda] Termination checking in cubical mode   Dr. ERDI Gergo
• [Agda] First Call for Papers: PACMPL issue ICFP 2019   Sam Tobin-Hochstadt
• [Agda] I want implicit coercions in Agda   Jesper Cockx
• [Agda] libraries for Bin   Sergei Meshveliani
• [Agda] overloading operations   James Wood
• [Agda] overloading operations   Guillaume Brunerie
• [Agda] overloading operations   Sergei Meshveliani
• [Agda] overloading operations   Sergei Meshveliani
• [Agda] overloading operations   Martín Hötzel Escardó
• [Agda] overloading operations   Guillaume Brunerie
• [Agda] overloading operations   Sergei Meshveliani
• [Agda] overloading operations   Guillaume Brunerie
• [Agda] overloading operations   Martin Escardo
• [Agda] overloading operations   Sergei Meshveliani
• [Agda] Does Agda have this axiom?   千里冰封
• [Agda] Termination checking in cubical mode   Dr. ERDI Gergo
• [Agda] overloading operations   Guillaume Allais
• [Agda] Agda Implementors' Meeting XXIX - Tokyo, March 13 -- 19, 2019   Youyou Cong
• [Agda] Call for Conference Grant Applications (Inclusiveness Target Countries)   Ambrus Kaposi
• [Agda] overloading operations   Sergei Meshveliani
• [Agda] cong with wildcard   Sergei Meshveliani
• [Agda] Homotopy Type Theory and Univalent Foundations conference in Oslo   Bjørn Ian Dundas
• [Agda] overloading operations   Guillaume Allais
• [Agda] overloading operations   Guillermo Calderon
• [Agda] overloading operations   Guillaume Brunerie
• [Agda] cong with wildcard   Nils Anders Danielsson
• [Agda] Does Agda have this axiom?   Nicolai Kraus
• [Agda] Does Agda have this axiom?   Apostolis Xekoukoulotakis
• [Agda] Does Agda have this axiom?   Martin Escardo
• [Agda] overloading operations   Sergei Meshveliani
• [Agda] overloading operations   Guillaume Allais
• [Agda] overloading operations   Sergei Meshveliani
• [Agda] overloading operations   Guillermo Calderon
• [Agda] I want implicit coercions in Agda   Miëtek Bak
• [Agda] I want implicit coercions in Agda   Sergei Meshveliani
• [Agda] "No instance"   Sergei Meshveliani
• [Agda] I want implicit coercions in Agda   Martin Escardo
• [Agda] I want implicit coercions in Agda   Miëtek Bak
• [Agda] I want implicit coercions in Agda   Martin Escardo
• [Agda] I want implicit coercions in Agda   Jon Sterling
• [Agda] I want implicit coercions in Agda   Peter Hancock
• [Agda] I want implicit coercions in Agda   Sergei Meshveliani
• [Agda] I want implicit coercions in Agda   Apostolis Xekoukoulotakis
• [Agda] I want implicit coercions in Agda   Stefan Monnier
• [Agda] "No instance"   Guillermo Calderón
• [Agda] "No instance"   Sergei Meshveliani
• [Agda] I want implicit coercions in Agda   Sergei Meshveliani
• [Agda] I want implicit coercions in Agda   Martin Escardo
• [Agda] I want implicit coercions in Agda   Ulf Norell
• [Agda] I want implicit coercions in Agda   Martin Escardo
• [Agda] I want implicit coercions in Agda   Jason -Zhong Sheng- Hu
• [Agda] What style of proof irrelevance do you prefer: annotated or inferred?   James Chapman
• [Agda] I want implicit coercions in Agda   Peter Hancock
• [Agda] I want implicit coercions in Agda   Apostolis Xekoukoulotakis
• [Agda] An error function and totality   Marko Dimjašević
• [Agda] An error function and totality   Philip Wadler
• [Agda] I want implicit coercions in Agda   Thorsten Altenkirch
• [Agda] I want implicit coercions in Agda   Thorsten Altenkirch
• [Agda] What style of proof irrelevance do you prefer: annotated or inferred?   Thorsten Altenkirch
• [Agda] I want implicit coercions in Agda   Guillaume Allais
• [Agda] I want implicit coercions in Agda   Sergei Meshveliani
• [Agda] I want implicit coercions in Agda   Sergei Meshveliani
• [Agda] [Fwd: Re: I want implicit coercions in Agda]   Sergei Meshveliani
• [Agda] An error function and totality   Marko Dimjašević
• [Agda] I want implicit coercions in Agda   Sergei Meshveliani
• [Agda] I want implicit coercions in Agda   Guillaume Brunerie
• [Agda] I want implicit coercions in Agda   Sergei Meshveliani
• [Agda] Some mistakes in the code on the 13th page of Pierre Kraft's thesis.   Serge Leblanc
• [Agda] An error function and totality   Philip Wadler
• [Agda] I want implicit coercions in Agda   Nils Anders Danielsson
• [Agda] An error function and totality   Nils Anders Danielsson
• [Agda] I want implicit coercions in Agda   Sergei Meshveliani
• [Agda] PhD positions in Computer Science at University of Bergen   Håkon Robbestad Gylterud
• [Agda] I want implicit coercions in Agda   Nicolas Pouillard
• [Agda] I want implicit coercions in Agda   Nils Anders Danielsson
• [Agda] Research positions in cryptography, blockchain, and formal verification at Aarhus   Bas Spitters
• [Agda] I want implicit coercions in Agda   Nicolas Pouillard
• [Agda] CoqPL 2019: Call for Participation   Robbert Krebbers
• [Agda] Programming Language Foundations in Agda   Philip Wadler
• [Agda] 10 PhD studentships in Nottingham   Graham Hutton
• [Agda] Type-checking errors with meta variables   François Thiré
• [Agda] installing on ghc-8.02   Sergei Meshveliani
• [Agda] installing on ghc-8.02   Andres Sicard Ramirez
• [Agda] installing on ghc-8.02   Sergei Meshveliani
• [Agda] installing on ghc-8.02   Andres Sicard Ramirez
• [Agda] Type-checking errors with meta variables   Jesper Cockx
• [Agda] installing on ghc-8.02   Sergei Meshveliani
• [Agda] using literals and the standard library   Martin Stone Davis
• [Agda] using literals and the standard library   Guillaume Allais
• [Agda] using literals and the standard library   Martin Stone Davis
• [Agda] using literals and the standard library   Guillaume Allais
• [Agda] using literals and the standard library   Martin Stone Davis
• [Agda] using literals and the standard library   Ulf Norell
• [Agda] using literals and the standard library   Jesper Cockx
• [Agda] using literals and the standard library   Matthew Daggitt
• [Agda] using literals and the standard library   Apostolis Xekoukoulotakis
• [Agda] using literals and the standard library   Martin Escardo
• [Agda] using literals and the standard library   Apostolis Xekoukoulotakis
• [Agda] using literals and the standard library   Thorsten Altenkirch
• [Agda] using literals and the standard library   Martin Escardo
• [Agda] Development lib vs 0.17   Sergei Meshveliani
• [Agda] internal error in Dev Dec 4   Sergei Meshveliani
• [Agda] internal error in Dev Dec 4   Ulf Norell
• [Agda] Development lib vs 0.17   Matthew Daggitt
• [Agda] bug reported   Sergei Meshveliani
• [Agda] UTF in Ubuntu   mechvel at scico.botik.ru
• [Agda] UTF in Ubuntu   Nils Anders Danielsson
• [Agda] UTF in Ubuntu   mechvel at scico.botik.ru
• [Agda] lost fixity of ≈   mechvel at scico.botik.ru
• [Agda] UTF in Ubuntu   Nils Anders Danielsson
• [Agda] lost fixity of ≈   Nils Anders Danielsson
• [Agda] Call for Conference Grant Applications (Inclusiveness Target Countries)   Ambrus Kaposi
• [Agda] TwoPhase refinement of TCommit in Agda : Some thoughts.   Apostolis Xekoukoulotakis
• [Agda] invert pattern matching   Martin Escardo
• [Agda] invert pattern matching   Ulf Norell
• [Agda] invert pattern matching   Martin Escardo
• [Agda] invert pattern matching   Nils Anders Danielsson
• [Agda] invert pattern matching   Martin Escardo
• [Agda] lost fixity of ≈   Andreas Källberg
• [Agda] lost fixity of ≈   Sergei Meshveliani
• [Agda] Congratulations to Jesper! --- [EAPLS] BOARD ANNOUNCEMENT: Jesper Cockx (KU Leuven) wins EAPLS PhD Disseration Award 2017/18]   Wolfram Kahl
• [Agda] Congratulations to Jesper! --- [EAPLS] BOARD ANNOUNCEMENT: Jesper Cockx (KU Leuven) wins EAPLS PhD Disseration Award 2017/18]   Jon Sterling
• [Agda] Congratulations to Jesper! --- [EAPLS] BOARD ANNOUNCEMENT: Jesper Cockx (KU Leuven) wins EAPLS PhD Disseration Award 2017/18]   Philip Wadler
• [Agda] Congratulations to Jesper! --- [EAPLS] BOARD ANNOUNCEMENT: Jesper Cockx (KU Leuven) wins EAPLS PhD Disseration Award 2017/18]   Martin Escardo
• [Agda] Congratulations to Jesper! --- [EAPLS] BOARD ANNOUNCEMENT: Jesper Cockx (KU Leuven) wins EAPLS PhD Disseration Award 2017/18]   Roman
• [Agda] Congratulations to Jesper! --- [EAPLS] BOARD ANNOUNCEMENT: Jesper Cockx (KU Leuven) wins EAPLS PhD Disseration Award 2017/18]   Apostolis Xekoukoulotakis
• [Agda] Congratulations to Jesper! --- [EAPLS] BOARD ANNOUNCEMENT: Jesper Cockx (KU Leuven) wins EAPLS PhD Disseration Award 2017/18]   James Chapman
• [Agda] Congratulations to Jesper! --- [EAPLS] BOARD ANNOUNCEMENT: Jesper Cockx (KU Leuven) wins EAPLS PhD Disseration Award 2017/18]   Jesper Cockx
• [Agda] Postdoc Positions at KTH and Chalmers on Cyber-Physical Systems (with CakeML)   Magnus Myreen
• [Agda] Automating Haskell FFI bindings   Caryo Scelus
• [Agda] SBLP 2019 - First call for papers   Rodrigo Ribeiro
• [Agda] Codata error   Sergei Meshveliani
• [Agda] Codata error   Caryo Scelus
• [Agda] Codata error   Sergei Meshveliani
• [Agda] Solver usage   Sergei Meshveliani

Last message date: Sun Dec 30 23:01:48 CET 2018
Archived on: Sun Dec 30 23:01:52 CET 2018

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