2020 Archives by thread
Starting: Wed Jan 1 13:02:27 CET 2020
Ending: Thu Dec 31 23:40:10 CET 2020
Messages: 966
- [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1
mechvel at scico.botik.ru
- [Agda] How experimental is Cumulativity?
Joey Eremondi
- [Agda] MSFP 2020 - Final Call for Papers
Max New
- [Agda] [TFP'20] draft paper deadline open (January 10 2020) Trends in Functional Programming 2020, 13-14 February, Krakow, Poland
Peter Achten
- [Agda] PhD Position in in Theory and Implementation of Dependently Typed Programming Languages
Jesper Cockx
- [Agda] CMCS 2020: Final Call for Papers (extended deadlines)
Henning Basold
- [Agda] LSFA 2020 Second call for papers
Ana Bove
- [Agda] a tutorial for proof by coinduction
Pierre Lescanne (en)
- [Agda] Precedence of arrow
Martin Escardo
- [Agda] [TFP'20] call for participation: Trends in Functional Programming 2020, 13-14 February, Krakow, Poland
Peter Achten
- [Agda] ETAPS Test of Time Award 2020, call for nominations
Tarmo Uustalu
- [Agda] First ETAPS Doctoral Dissertation Award, final call for nominations
Tarmo Uustalu
- [Agda] delaying computation to run time
mechvel at scico.botik.ru
- [Agda] Coinductive records and separate files in Agda
William Harrison
- [Agda] When I try to reduce, I get a meta. (Reflection).
Apostolis Xekoukoulotakis
- [Agda] tracing & profiling
mechvel at scico.botik.ru
- [Agda] 10 PhD studentships in Nottingham for Home/EU applicants
Graham Hutton
- [Agda] Struggling with irrelevance
Mathijs Kwik
- [Agda] equality on Char
mechvel at scico.botik.ru
- [Agda] Unbound level variables in rewrite rule
Filippo Sestini
- [Agda] type checking in real-world algebra
mechvel at scico.botik.ru
- [Agda] Rewrite rules for both Set and Prop
Filippo Sestini
- [Agda] Call for Papers: PACMPL issue ICFP 2020
Sam Tobin-Hochstadt
- [Agda] consistency
Patricia Peratto
- [Agda] [2.6.1] erasure and irrelevance unpredictable
Mathijs Kwik
- [Agda] status of inlining agda code
Thorsten Altenkirch
- [Agda] agda latex mode
Thorsten Altenkirch
- [Agda] Contributing: good first issues
Nils Anders Danielsson
- [Agda] Getting started: Emacs
Vox Veritatis
- [Agda] Getting started: couple more questions
Vox Veritatis
- [Agda] TEASE-LP (co-located with ETAPS 2020): Second call for contributions
Henning Basold
- [Agda] Termination checking with Lexicographic recursive calls
Sergey Goncharov
- [Agda] Agda Documentation
Panos Ked
- [Agda] TERMGRAPH 2020: Call for papers
Patrick Bahr
- [Agda] CFP: Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2020), with special session in honour of Frank Pfenning
Claudio Sacerdoti Coen
- [Agda] CFP: LSFA 2020
Ana Bove
- [Agda] recursion, lexicographic ordering
Siek, Jeremy
- [Agda] let vs where
Thorsten Altenkirch
- [Agda] Agda on Github Pages
Ed Nutting
- [Agda] why coinductive?
Thorsten Altenkirch
- [Agda] PPDP 2020 Call For Papers
Andreas Abel
- [Agda] PPDP 2020 Call For Papers (corrected link)
Andreas Abel
- [Agda] Why dependent type theory?
Jason Gross
- [Agda] [Coq-Club] Why dependent type theory? (resend)
Thorsten Altenkirch
- [Agda] What to do when Rewrite fails?
Joey Eremondi
- [Agda] add to the Agda group on Github
Jason -Zhong Sheng- Hu
- [Agda] what is happening here?
Thorsten Altenkirch
- [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 2
Andrés Sicard-Ramírez
- [Agda] Agda meeting postponed [Fwd: AIM XXXI Postponed]
Andreas Abel
- [Agda] [ANNOUNCE] Agda 2.6.1
Andrés Sicard-Ramírez
- [Agda] [ANNOUNCE] Standard library v1.3
Matthew Daggitt
- [Agda] LSFA 2020 - Deadline Extension
Ana Bove
- [Agda] package agda-mode not working
Michel Levy
- [Agda] idiom brackets in 2.6.1
mechvel at scico.botik.ru
- [Agda] failure of cabal install Agda
Michel Levy
- [Agda] PhD positions in Computational Mathematics at Stockholm University
Anders Mortberg
- [Agda] exercice of Peter Dybjer
Michel Levy
- [Agda] "Not in Scope" definitional equalities
Sergey Goncharov
- [Agda] where is the official agda.sty
Michel Levy
- [Agda] syntax declaration
Michel Levy
- [Agda] Multiple Research Positions (3 Doctoral, 5 Post-doctoral) on AI Verification
Robert Atkey
- [Agda] How can I implement naive sized lambdas?
Georgi Lyubenov
- [Agda] 2nd Workshop on Formal Methods for Blockchains (FMBC) 2020 - 1st CFP
Bruno Bernardo
- [Agda] splitting cases
Thorsten Altenkirch
- [Agda] error message in agda
Michel Levy
- [Agda] rewrite keyword
Michel Levy
- [Agda] TERMGRAPH 2020: 2nd Call for papers
Patrick Bahr
- [Agda] Filling squares
James Wood
- [Agda] free download of VFPIA
Aaron Stump
- [Agda] Two PhD positions in Utrecht
Wouter Swierstra
- [Agda] Example of an online conference in theoretical computer science BCTCS starting now
Setzer A.G.
- [Agda] ML Family Workshop 2020: Call for presentations
Leo White
- [Agda] Update on Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'20) on July 5-6, 2020
Benedikt Ahrens
- [Agda] Induction from Sigma?
Joey Eremondi
- [Agda] Installing standard and plfa libraries
Michel Levy
- [Agda] Formalization of a system dependently-typed records in Agda?
Jacques Carette
- [Agda] commutative ring solver
mechvel at scico.botik.ru
- [Agda] Automatic conversion between records and iterated Sigma types
Martin Escardo
- [Agda] TERMGRAPH 2020: Deadline Extension - 22 April
Patrick Bahr
- [Agda] L and inverted L characters
Philippe de Rochambeau
- [Agda] error in plfa exercise
Michel Levy
- [Agda] Compiling HelloWorld
Philippe de Rochambeau
- [Agda] StringOrInt function
Philippe de Rochambeau
- [Agda] First-Class Type Issue
Philippe de Rochambeau
- [Agda] Certified Programs and Proofs (CPP) 2021: First Call for Papers
Andrei Popescu
- [Agda] Online Agda meeting?
Nils Anders Danielsson
- [Agda] words
Philippe de Rochambeau
- [Agda] plfa, using proj2, missing in Quantifiers
Michel Levy
- [Agda] Universe level in heterogeneous association list
Nicolas Osborne
- [Agda] Introducing hypotheses
Philippe de Rochambeau
- [Agda] problem with proj1
Michel Levy
- [Agda] An article by Jean-Yves Girard
Philippe de Rochambeau
- [Agda] bottom and false
Patricia Peratto
- [Agda] Strict equality _≣_ in agda
Herminie Pagel
- [Agda] FMBC 2020: 2nd Workshop on Formal Methods for Blockchains (CfP, Deadline Extension)
Bruno Bernardo
- [Agda] "bug" on x = x
mechvel at scico.botik.ru
- [Agda] Nat Fuel vs Sized Types (and other Sized Type questions)
Joey Eremondi
- [Agda] What do you use for variable binding in 2020?
Joey Eremondi
- [Agda] --rewriting and the Agda standard library
Siek, Jeremy
- [Agda] Transcendental Syntax
phiroc at free.fr
- [Agda] Agda Implementors' Meeting XXXII
Nils Anders Danielsson
- [Agda] a strange function type report
mechvel at scico.botik.ru
- [Agda] Light grey background?
Jakob von Raumer
- [Agda] Two assistant/associate professor positions in PL at TU Delft
Jesper Cockx
- [Agda] Introducing Agdapad, a website for real-time collaborative Agda experiments (early preview)
Ingo Blechschmidt
- [Agda] PhD position at University of Birmingham, UK
Benedikt Ahrens
- [Agda] Question about colists, musical notation vs coinductive records, and all that
William Harrison
- [Agda] Termination Checking and WIthout-K
Joey Eremondi
- [Agda] WFLP 2020 CFP (Workshop on Functional and Constraint Logic Programming)
Claudio Sacerdoti Coen
- [Agda] why is this corecursion red? And indexed coinductive definitions.
Thorsten Altenkirch
- [Agda] lost in modules
Michel Levy
- [Agda] Agda patterns
Martin Escardo
- [Agda] ICFP 2020 will be held ONLINE Aug 23-28
Sam Tobin-Hochstadt
- [Agda] install agda
Michel Levy
- [Agda] installation trouble WAS Re: why is this corecursion red? And indexed coinductive definitions.
Thorsten Altenkirch
- [Agda] Boolean And in Pair
Philippe de Rochambeau
- [Agda] Journal of Functional Programming - Call for PhD Abstracts
Graham Hutton
- [Agda] PPDP 2020 Final call for papers
Andreas Abel
- [Agda] _≡⟨_⟩_ operator
Philippe de Rochambeau
- [Agda] FMBC 2020: 2nd Workshop on Formal Methods for Blockchains (3rd CfP, Deadline Extension)
Bruno Bernardo
- [Agda] TyDe 2020 - Final Call for Papers
Cyrus Omar
- [Agda] "Failed to find source"
mechvel at scico.botik.ru
- [Agda] Call for Contributions: Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'20) on July 5-6, 2020
Benedikt Ahrens
- [Agda] Data.Thunk, cofix question
William Harrison
- [Agda] how to evaluate in the current context
Thorsten Altenkirch
- [Agda] with + Path
Thorsten Altenkirch
- [Agda] PPDP 2020 deadline extension
Andreas Abel
- [Agda] ML Family Workshop 2020: Deadline extension
Leo White
- [Agda] PhD Scholarships in Mathematics and computation
Martin Escardo
- [Agda] Milestone-Based Paid Remote Short-Term Projects in Formalization of Algorithms
Mateus de Oliveira Oliveira
- [Agda] Value-recursive records?
Joey Eremondi
- [Agda] Performance: opening parameterized modules before the fields of a record
Guillaume Brunerie
- [Agda] Call for Papers: APLAS 2020
Bruno Oliveira
- [Agda] Understanding Glue
Thorsten Altenkirch
- [Agda] Problem proving inequality with HeterogeneousEquality
Shin-Cheng Mu
- [Agda] convertibility of implicit and explicit Pi-types
Thorsten Altenkirch
- [Agda] how do I quote agda code on the agda wiki?
Thorsten Altenkirch
- [Agda] problem with install Agda
Michel Levy
- [Agda] A preliminary programme for AIM XXXII
Nils Anders Danielsson
- [Agda] AGDA XXXII has started
Thorsten Altenkirch
- [Agda] installation problem
Michel Levy
- [Agda] Rewriting rules in parametrized modules
Andrej Tokarčík
- [Agda] Call for Submissions: ICFP Student Research Competition
Sam Tobin-Hochstadt
- [Agda] What does does it mean if "-invert730" shows up in a goal?
Joey Eremondi
- [Agda] several agda versions
Thorsten Altenkirch
- [Agda] many ways to import the same thing from record
mechvel at scico.botik.ru
- [Agda] First call for draft papers for IFL 2020 (Implementation and Application of Functional Languages)
Jurriaan Hage
- [Agda] Strange bug
Pierre Lescanne
- [Agda] ETAPS 2020 afternoon, online, 2 July 2020, call for participation
Tarmo Uustalu
- [Agda] Call for Tutorial Proposals: ICFP 2020
Sam Tobin-Hochstadt
- [Agda] "not in scope" without "does not export"
mechvel at scico.botik.ru
- [Agda] "Cannot resolve" vs "Multiple definition"
mechvel at scico.botik.ru
- [Agda] "open" in record telescope
mechvel at scico.botik.ru
- [Agda] LFMTP2020 Call for Participation
Claudio Sacerdoti Coen
- [Agda] Defining equality in Prop
Bob Atkey
- [Agda] Call for Participation: HoTT/UF 2020 - July 5-7
Benedikt Ahrens
- [Agda] TERMGRAPH 2020: Call for (Online) Participation
Patrick Bahr
- [Agda] Final Call for Papers: APLAS 2020 (deadline on the 6th of July)
Bruno Oliveira
- [Agda] Why is this non-terminating?
Jinwoo Lee
- [Agda] Moving Prop under Quantifiers?
Joey Eremondi
- [Agda] Permanent positions at the University of Strathclyde
Fredrik Nordvall Forsberg
- [Agda] FMBC 2020 - Call for Participation
Bruno Bernardo
- [Agda] Cabal hell again
Thorsten Altenkirch
- [Agda] unfolding just a single definition in the context of a goal
Marcus Christian Lehmann
- [Agda] Call for Participation: ICFP 2020
Sam Tobin-Hochstadt
- [Agda] Second call for draft papers for IFL 2020 (Implementation and Application of Functional Languages)
Jurriaan Hage
- [Agda] Final Call for Tutorials, Discussions, and Social Events: ICFP 2020
Sam Tobin-Hochstadt
- [Agda] Problem with generalised variables
Thorsten Altenkirch
- [Agda] ETAPS 2021 1st joint call for papers
Tarmo Uustalu
- [Agda] Emacs mode setup command failing.
David Banas
- [Agda] List of fonts required for Emacs mode?
David Banas
- [Agda] Shadowing definitions
Thorsten Altenkirch
- [Agda] CMCS 2020: Call for Participation
Henning Basold
- [Agda] Second Call for Participation: ICFP 2020
Sam Tobin-Hochstadt
- [Agda] Call for Tutorial Participation: ICFP 2020
Sam Tobin-Hochstadt
- [Agda] problem with algebraic hierarchy
mechvel at scico.botik.ru
- [Agda] Third call for draft papers for IFL 2020 (Implementation and Application of Functional Languages)
Jurriaan Hage
- [Agda] MSFP 2020 (Monday August 31st and Tuesday September 1st) - Call for Participation
Max New
- [Agda] Weird termination problem
Thorsten Altenkirch
- [Agda] \ell does not display
Pierre Lescanne (en)
- [Agda] rewrite construct not working, when Naturals defined locally?
David Banas
- [Agda] Certified Programs and Proofs (CPP) 2021: Final Call for Papers
Andrei Popescu
- [Agda] Has Agda been tested on i686 architecture ?
Pierre Lescanne (en)
- [Agda] type-checking x=x
mechvel at scico.botik.ru
- [Agda] Third Call for Participation: ICFP 2020
Sam Tobin-Hochstadt
- [Agda] Hanging out with the Lean crowd
Carette, Jacques
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
Jesper Cockx
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
Manuel Bärenz
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
Nils Anders Danielsson
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
Jesper Cockx
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
Jesper Cockx
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
David Thrane Christiansen
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
Manuel Bärenz
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
Nils Anders Danielsson
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
Jesper Cockx
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
Carette, Jacques
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
Andreas Källberg
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
a.j.rouvoet
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
Jesper Cockx
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
a.j.rouvoet
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
David Thrane Christiansen
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
Georgi Lyubenov
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
James Wood
- [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)
Jesper Louis Andersen
- [Agda] Question, re: x-dual-U exercise in Negation chapter of PLFA.
David Banas
- [Agda] PLFA - Negation - Exercise Classical
David Banas
- [Agda] First and Only Call for Participation for IFL 2020 (Implementation and Application of Functional Languages)
Jurriaan Hage
- [Agda] 2 tips for my fellow Agda newbies
David Banas
- [Agda] Overloaded constructor trouble
Thorsten Altenkirch
- [Agda] A philosophical question on absurd.
David Banas
- [Agda] multiple instance resolution and negation
Marcus Christian Lehmann
- [Agda] BOPL / PPDP 2020 call for participation (register until 3 Sep)
Andreas Abel
- [Agda] strangely cannot reproduce a report
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda Standard Library 1.4 release candidate 1
Matthew Daggitt
- [Agda] bug?
mechvel at scico.botik.ru
- [Agda] LFMTP 2020 Post-Proceedings: Call for Papers
Claudio Sacerdoti Coen
- [Agda] Question about transport and cubical
Manuel Bärenz
- [Agda] Fwd: Question about transport and cubical
Manuel Bärenz
- [Agda] Fwd: Fwd: Question about transport and cubical
Manuel Bärenz
- [Agda] Resolving a universe level problem
Marko Dimjašević
- [Agda] Multi-line comments in literate Agda files
Marko Dimjašević
- [Agda] Size Issue when Modelling Effectful Data Structures and Computations
jonas.hoefer at stud.htwk-leipzig.de
- [Agda] Agda Implementors' Meeting XXXIII: Call for talks and participation
Jesper Cockx
- [Agda] [ANNOUNCE] Agda 2.6.1.1
Ulf Norell
- [Agda] Info about instance resolution in macro
Joris Ceulemans
- [Agda] CPP 2021 abstract deadline due soon (in ~23 hours)
Andrei Popescu
- [Agda] [ANNOUNCE] Standard library v1.4
Matthew Daggitt
- [Agda] ETAPS 2021 2nd joint call for papers
Tarmo Uustalu
- [Agda] Agda and machine learning
Warrick Macmillan
- [Agda] Suspicious normalisation
Marko Dimjašević
- [Agda] testing Agda-2.6.1 on a large project
mechvel at scico.botik.ru
- [Agda] [TFP'21] first call for papers: Trends in Functional Programming 2021, 17-19 February (with Lambda Days 2021 & TFPIE 2021)
Peter Achten
- [Agda] Why the light gray highlighting here?
David Banas
- [Agda] [TFPIE'21] First Call For Papers: Trends in Functional Programming *in Education* 2021, 16 February (with Lambda Days 2021 & TFP 2021)
Peter Achten
- [Agda] Bit-wise XOR for Word64?
David Banas
- [Agda] Verifying type inference in Agda?
William Harrison
- [Agda] Help with stuck unification/intrinsic typing in general
Daniel Lee
- [Agda] Question about inequality and absurd patterns
William Harrison
- [Agda] nontermination and Sized types
vlad
- [Agda] termination problem
mechvel at scico.botik.ru
- [Agda] ETAPS 2021 final joint call for papers
Tarmo Uustalu
- [Agda] Help with understanding REWRITE
Andrew M. Pitts
- [Agda] a strange "unsolved" report
mechvel at scico.botik.ru
- [Agda] Using Haskell type class constraints with Agda types
Alexander Ben Nasrallah
- [Agda] CfP for TYPES 2020 postproceedings:
Ugo de'Liguoro
- [Agda] slightly wrong sized datatype definition leads to proof of False
Vlad Rusu
- [Agda] F-IDE 2021 - Call for Papers
Andrei Paskevich
- [Agda] agda2lagda (Halloween edition): Agda for the illiterate
Andreas Abel
- [Agda] Converting intrinsically typed terms
rozowski w.k. (wkr1u18)
- [Agda] Negative coinductive sized types
Florian Engel
- [Agda] A tutorial on inference in Agda
Roman
- [Agda] Call for Workshop Proposals: ICFP 2021
Sam Tobin-Hochstadt
- [Agda] General notion of equality for syntactically equal objects with different types from the same datatype family?
Matthew Daggitt
- [Agda] Inference difficulties
Conal Elliott
- [Agda] Three new Teaching Assistant positions in Nottingham
Graham Hutton
- [Agda] Teaching positions at Nottingham
Thorsten Altenkirch
- [Agda] APLAS 2020 Call for Participation
Bruno Oliveira
- [Agda] two proof-assistant friendly posts of Lecturer in Cybersecurity at University of Sheffield: deadline 3rd December 2020
Andrei Popescu
- [Agda] when to set underscore suffix?
mechvel at scico.botik.ru
- [Agda] forced arguments in EqReasoning
mechvel at scico.botik.ru
- [Agda] fully funded PhD position at University of Sheffield on the formal verification of industrial robots
Andrei Popescu
- [Agda] Agda on raspberry pi 4
Martin Escardo
- [Agda] Agda Interactive Notebooks
Andrea Amantini
- [Agda] Isomorphisms, equational reasoning, and level changes
Conal Elliott
- [Agda] Weird instance propagation between parameterised modules
Orestis Melkonian
- [Agda] [TFP'21] second call for papers: Trends in Functional Programming 2021, 18-19 February (online event with Lambda Days 2021 & TFPIE 2021)
Peter Achten
- [Agda] Tips for working around proof relevance
Daniel Lee
- [Agda] agda-categories, a story
Carette, Jacques
- [Agda] PhD studentships in Robotics (Edinburgh Center for Robotics)
Ekaterina Komendantskaya
- [Agda] installing agda
Patricia Peratto
- [Agda] [TFPIE'21] Second Call For Papers: Trends in Functional Programming *in Education* 2021, 16 February 2021 (with Lambda Days 2021 & TFP 2021)
Peter Achten
- [Agda] irrelevancy annotation
mechvel at scico.botik.ru
- [Agda] CPP 2021: Call for Participation and Lightning Talks
Andrei Popescu
- [Agda] Why are some terms in the Agda goal report colored blue?
David Banas
Last message date:
Thu Dec 31 23:40:10 CET 2020
Archived on: Thu Dec 31 23:40:27 CET 2020
This archive was generated by
Pipermail 0.09 (Mailman edition).