2021 Archives by subject
Starting: Sun Jan 3 15:26:27 CET 2021
Ending: Wed Dec 29 12:27:50 CET 2021
Messages: 394
- [Agda] --exact-split
Martin Escardo
- [Agda] --exact-split
Tom Jack
- [Agda] --program-suffix using stack
Andreas Nuyts
- [Agda] -rtsopts
mechvel at scico.botik.ru
- [Agda] -rtsopts
Nils Anders Danielsson
- [Agda] -rtsopts
mechvel at scico.botik.ru
- [Agda] 1+2 Assistant positions at Chalmers on ICT and Basic Science
Ana Bove
- [Agda] 10 PhD studentships in Nottingham
Graham Hutton
- [Agda] 10 PhD studentships in Nottingham
Graham Hutton
- [Agda] 21st Midlands Graduate School in the Foundations of Computing Science: Call for Participation
Andrei Popescu
- [Agda] 21st Midlands Graduate School in the Foundations of Computing Science: Final Call for Participation
Andrei Popescu
- [Agda] 2nd Call for Contributions: (Virtual) Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'21) on July 17-18, 2021
Benedikt Ahrens
- [Agda] 2nd Call for Papers: FLOPS 2022
Michael Hanus
- [Agda] 30 months postdoctoral research position at University of Sheffield involving proof-assistant-based verification -- application deadline 23 Sept. 2021
Andrei Popescu
- [Agda] 3 Fully funded PhD positions in Software Technology at Radboud University, Netherlands
Peter Achten
- [Agda] 7th International Workshop on Proof eXchange for Theorem Proving (PxTP) - DEADLINE EXTENSION: May 5
Chantal Keller
- [Agda] 7th International Workshop on Proof eXchange for Theorem Proving (PxTP) - First CFP
Chantal Keller
- [Agda] 7th International Workshop on Proof eXchange for Theorem Proving (PxTP) - Second CFP
Chantal Keller
- [Agda] [ANNOUNCE] Agda 2.6.1.2
Andrés Sicard-Ramírez
- [Agda] [ANNOUNCE] Agda 2.6.1.3
Andrés Sicard-Ramírez
- [Agda] [ANNOUNCE] Agda 2.6.2
Andrés Sicard-Ramírez
- [Agda] [ANNOUNCE] Agda 2.6.2
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2
Andrés Sicard-Ramírez
- [Agda] [ANNOUNCE] Agda 2.6.2
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2
Andrés Sicard-Ramírez
- [Agda] [ANNOUNCE] Agda 2.6.2
Andrew Pitts
- [Agda] [ANNOUNCE] Agda 2.6.2
Andreas Abel
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
Andreas Abel
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
Andreas Abel
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
Nils Anders Danielsson
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
Nils Anders Danielsson
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
Andreas Abel
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
Andreas Abel
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
Nils Anders Danielsson
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate
Nils Anders Danielsson
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate
Andrés Sicard-Ramírez
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate
Jesper Cockx
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate
Jesper Cockx
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate
Andrés Sicard-Ramírez
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate
Jesper Cockx
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate
Nils Anders Danielsson
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
Andrés Sicard-Ramírez
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
Martin Escardo
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
Nils Anders Danielsson
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
Andrés Sicard-Ramírez
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
Nils Anders Danielsson
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
Nils Anders Danielsson
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Standard library v1.5
Matthew Daggitt
- [Agda] [ANNOUNCE] Standard library v1.5 - release candidate 1
Matthew Daggitt
- [Agda] [ANNOUNCE] Standard library v1.5 - release candidate 1
mechvel at scico.botik.ru
- [Agda] [ANNOUNCE] Standard library v1.5 - release candidate 1
a.j.rouvoet
- [Agda] [ANNOUNCE] Standard library v1.6
Matthew Daggitt
- [Agda] [ANNOUNCE] Standard library v1.6 - release candidate 1
Matthew Daggitt
- [Agda] [ ANNOUNCE ] Standard library v1.7 - release candidate 1
Matthew Daggitt
- [Agda] [ ANNOUNCE ] Standard library v1.7 - release candidate 2
Matthew Daggitt
- [Agda] [ ANNOUNCE ] Standard library v1.7 - release candidate 2
mechvel at scico.botik.ru
- [Agda] [ ANNOUNCE ] Standard library version 1.7
Matthew Daggitt
- [Agda] [CFP] Logical Frameworks and Meta-Languages: Theory and Practice
Enrico Tassi
- [Agda] [CFP] Logical Frameworks and Meta-Languages: Theory and Practice - Extended Deadline
Enrico Tassi
- [Agda] [HoTT] Reminder: 2 year position on HoTT and related topics in Stockholm, deadline Friday next week
Guillaume Brunerie
- [Agda] [Lambda Days + TFP + TFPIE 2021] call for participation
Peter Achten
- [Agda] [RFC stdlib v2.0] 1. Numeric ops with non-zero proofs
Matthew Daggitt
- [Agda] [RFC stdlib v2.0] 1. Numeric ops with non-zero proofs
Matthew Daggitt
- [Agda] [RFC stdlib v2.0] 2. Numeric proofs which restrict their arguments to be positive/non-negative etc.
Matthew Daggitt
- [Agda] [TFP'21] final call for papers: Trends in Functional Programming 2021, 17-19 February (online event with Lambda Days 2021 & TFPIE 2021)
Peter Achten
- [Agda] [TFP'22] first call for papers: Trends in Functional Programming 2022, 10-11 February (with Lambda Days 2022 & TFPIE 2022)
Peter Achten
- [Agda] [TFPIE'21] Third and Final Call For Papers: Trends in Functional Programming *in Education* 2021, 16 February 2021 (with Lambda Days 2021 & TFP 2021)
Peter Achten
- [Agda] [TYPES] Congruence rules vs frames
Siek, Jeremy
- [Agda] [TYPES] Congruence rules vs frames
Philip Wadler
- [Agda] `making' application
mechvel at scico.botik.ru
- [Agda] `making' application
mechvel at scico.botik.ru
- [Agda] Absurd patterns and HoTT
Felix Cherubini
- [Agda] Absurd patterns and HoTT
Martin Escardo
- [Agda] Absurd patterns and HoTT
Dan Doel
- [Agda] Absurd patterns and HoTT
Felix Cherubini
- [Agda] Absurd patterns and HoTT
Jesper Cockx
- [Agda] Absurd patterns and HoTT
Martin Escardo
- [Agda] Absurd patterns and HoTT
Jesper Cockx
- [Agda] agda-categories, a story
Harley D. Eades III
- [Agda] Agda Implementors' Meeting XXXIV: Call for talks and participation
Jesper Cockx
- [Agda] Agda Implementors' Meeting XXXIV: Call for talks and participation
Jacques Carette
- [Agda] Agda on Apple Silicon?
Kenichi Asai
- [Agda] Agda on Apple Silicon?
Ettore Aldrovandi
- [Agda] Agda on Apple Silicon?
Andreas Källberg
- [Agda] Agda on Apple Silicon?
Martin Escardo
- [Agda] Agda on Apple Silicon?
Conal Elliott
- [Agda] Agda on Apple Silicon?
Conal Elliott
- [Agda] Agda on Apple Silicon?
Kenichi Asai
- [Agda] Agda on Apple Silicon?
Martin Escardo
- [Agda] Agda on Apple Silicon?
Liang-Ting Chen
- [Agda] Agda on Apple Silicon?
Martin Escardo
- [Agda] agda under windows WSL
Anton Setzer
- [Agda] agda under windows WSL
Jason Hu
- [Agda] agda under windows WSL
Anton Setzer
- [Agda] agda under windows WSL
Jason Hu
- [Agda] agda under windows WSL
Xuanrui Qi
- [Agda] agda under windows WSL
Xuanrui Qi
- [Agda] agda under windows WSL
Anton Setzer
- [Agda] agda under windows WSL
Nils Anders Danielsson
- [Agda] Alectryon - My first case of Coq envy
Carette, Jacques
- [Agda] Alectryon - My first case of Coq envy
Andrew Pitts
- [Agda] Alectryon - My first case of Coq envy
Martin Escardo
- [Agda] another level problem
Siek, Jeremy
- [Agda] another level problem
Siek, Jeremy
- [Agda] another level problem
Jason -Zhong Sheng- Hu
- [Agda] another level problem
András Kovács
- [Agda] another level problem
Siek, Jeremy
- [Agda] another level problem
Peter Hancock
- [Agda] another level problem
András Kovács
- [Agda] A question about the innards of C-c C-d
Eduardo Ochs
- [Agda] A question on why "postulate" works but "variable" fails
Eduardo Ochs
- [Agda] A question on why "postulate" works but "variable" fails
Jesper Cockx
- [Agda] A question on why "postulate" works but "variable" fails
Eduardo Ochs
- [Agda] A question on why "postulate" works but "variable" fails
Jesper Cockx
- [Agda] Assistant/Associate Professorships in Nottingham
Graham Hutton
- [Agda] Assistant Professor of Software Technology (tenure track) at Radboud University
Robbert Krebbers
- [Agda] a stuck cubical Agda proof
Jason -Zhong Sheng- Hu
- [Agda] a stuck cubical Agda proof
Ayberk Tosun
- [Agda] a stuck cubical Agda proof
Jason -Zhong Sheng- Hu
- [Agda] Bizzare error
Philip Wadler
- [Agda] Bizzare error
James Wood
- [Agda] Bizzare error
Philip Wadler
- [Agda] Bizzare error
Andreas Abel
- [Agda] Bizzare error
Philip Wadler
- [Agda] Call by name vs call by need
Swierstra, W.S. (Wouter)
- [Agda] Call for Contributions: (Virtual) Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'21) on July 17-18, 2021
Benedikt Ahrens
- [Agda] Call for papers - Workshop on Type-Driven Development (TyDe 2021) at ICFP 2021
Josh Ko
- [Agda] Call for Papers: Fifth Workshop on Formal Mathematics for Mathematicians (FMM 2021)
Andrei Popescu
- [Agda] Call for Papers: FLOPS 2022
Shin-Cheng Mu
- [Agda] Call for Papers: PACMPL issue ICFP 2021
Sam Tobin-Hochstadt
- [Agda] Call for Participation: ICFP 2021
Sam Tobin-Hochstadt
- [Agda] Call for participation: ML Family Workshop 2021
Jonathan Protzenko
- [Agda] Call for Participation: PPDP & LOPSTR 2021
Niccolò Veltri
- [Agda] Call for Tutorial, Panel, and Discussion Proposals: ICFP 2021
Sam Tobin-Hochstadt
- [Agda] Call for Workshop Proposals: ICFP 2022
Ilya Sergey
- [Agda] Certified Programs and Proofs (CPP) 2022: Call for Papers
Andrei Popescu
- [Agda] Certified Programs and Proofs (CPP) 2022: Call for Participation
Andrei Popescu
- [Agda] Certified Programs and Proofs (CPP) 2022: Final Call for Papers
Andrei Popescu
- [Agda] CfP: 14th Interaction and Concurrency Experience (ICE 2021)
Uma Zalakain (PGR)
- [Agda] CfP: CompLingInfoReasAI'21 / Computational Linguistics, Information, Reasoning, and AI 2021
Ana Bove
- [Agda] CFP: SLE 2021 - 14th ACM SIGPLAN International Conference on Software Language Engineering
Andrei Chis
- [Agda] CFP ICTCS 2021 - 22th Italian Conference on Theoretical Computer Science
Claudio Sacerdoti Coen
- [Agda] Chapter "Traps"
mechvel at scico.botik.ru
- [Agda] comparing performance to Coq
mechvel at scico.botik.ru
- [Agda] Compilation of Parser.y depends on the locale on Debian too
Eduardo Ochs
- [Agda] Compilation of Parser.y depends on the locale on Debian too
Andrés Sicard-Ramírez
- [Agda] Congruence rules vs frames
Philip Wadler
- [Agda] Congruence rules vs frames
Uma Zalakain (PGR)
- [Agda] convenient induction on non-empty list?
Jason Hu
- [Agda] convenient induction on non-empty list?
Matthew Daggitt
- [Agda] convenient induction on non-empty list?
James Smith
- [Agda] convenient induction on non-empty list?
Jason Hu
- [Agda] convenient induction on non-empty list?
Peter LeFanu Lumsdaine
- [Agda] Cubical: "show", and families over HITs
Andreas Nuyts
- [Agda] Cubical: "show", and families over HITs
Andreas Nuyts
- [Agda] Cubical: "show", and families over HITs
Evan Cavallo
- [Agda] Cubical Agda: injection is bijection to restricted codomain
Vlad Rusu
- [Agda] Cubical Agda: injection is bijection to restricted codomain
Guillaume Brunerie
- [Agda] Cubical Agda: injection is bijection to restricted codomain
Vlad Rusu
- [Agda] Cubical Agda: injection is bijection to restricted codomain
Guillaume Brunerie
- [Agda] Definition of Modal Operators
Lukas Stoll
- [Agda] dependent equality in Cubical Agda
Vlad Rusu
- [Agda] dependent equality in Cubical Agda
James Wood
- [Agda] dependent equality in Cubical Agda
Vlad Rusu
- [Agda] Dimension-safe matrix operations?
Kenichi Asai
- [Agda] Dimension-safe matrix operations?
Manuel Bärenz
- [Agda] Dimension-safe matrix operations?
Peter Thiemann
- [Agda] Dimension-safe matrix operations?
Matthew Daggitt
- [Agda] Eta for Bool
Swierstra, W.S. (Wouter)
- [Agda] Eta for Bool
Ulf Norell
- [Agda] ETAPS 2022 1st joint call for papers
Tarmo Uustalu
- [Agda] ETAPS 2022 2nd joint call for papers
Tarmo Uustalu
- [Agda] ETAPS 2022 final call for papers
Tarmo Uustalu
- [Agda] ETAPS Test of Time Award 2021, call for nominations
Tarmo Uustalu
- [Agda] ETAPS Test of Time Award 2022, call for nominations
Tarmo Uustalu
- [Agda] EuroProofNet - Call for Working Group membership Application
Frédéric Blanqui
- [Agda] Evaluation question
Martin Escardo
- [Agda] Evaluation question
mechvel at scico.botik.ru
- [Agda] Evaluation question
Ulf Norell
- [Agda] Evaluation question
Ulf Norell
- [Agda] Evaluation question
Ulf Norell
- [Agda] Evaluation question
Martin Escardo
- [Agda] Evaluation question
Ulf Norell
- [Agda] Evaluation question
Martin Escardo
- [Agda] expensive `with'
mechvel at scico.botik.ru
- [Agda] expensive `with'
James Wood
- [Agda] F-IDE 2021 - 2nd Call for Papers
Andrei Paskevich
- [Agda] F-IDE 2021 - Last Call for Papers - Extended Deadline
Andrei Paskevich
- [Agda] FMBC 2021 - 2nd Call for Papers
Bruno Bernardo
- [Agda] FMBC 2021 - 3rd Call for Papers (Deadline extensions)
Bruno Bernardo
- [Agda] FMBC 2021 - Call for Papers
Bruno Bernardo
- [Agda] FMBC 2021 - Call for Participation
Bruno Bernardo
- [Agda] FMBC 2021 - Final Call for Papers (Deadline extension)
Bruno Bernardo
- [Agda] fully funded PhD position on verification of industrial robots at University of Sheffield -- application deadline coming soon (Jan. 13)
Andrei Popescu
- [Agda] help with inductive sized types
James Smith
- [Agda] help with inductive sized types
Jonathan Chan
- [Agda] help with inductive sized types
Andreas Abel
- [Agda] help with inductive sized types
James Smith
- [Agda] How to validate eta-reduction in equational reasoning proofs?
David Banas
- [Agda] How to validate eta-reduction in equational reasoning proofs?
Jason -Zhong Sheng- Hu
- [Agda] How to validate eta-reduction in equational reasoning proofs?
Jesper Cockx
- [Agda] How to validate eta-reduction in equational reasoning proofs?
James Wood
- [Agda] How to validate eta-reduction in equational reasoning proofs?
Ulf Norell
- [Agda] How to validate eta-reduction in equational reasoning proofs?
David Banas
- [Agda] How to validate eta-reduction in equational reasoning proofs?
Oleg Grenrus
- [Agda] How to validate eta-reduction in equational reasoning proofs?
David Banas
- [Agda] How to validate eta-reduction in equational reasoning proofs?
Oleg Grenrus
- [Agda] How to validate eta-reduction in equational reasoning proofs?
David Banas
- [Agda] How to validate eta-reduction in equational reasoning proofs?
James Wood
- [Agda] How to write a type alias for _->_?
David Banas
- [Agda] How to write a type alias for _->_?
James Wood
- [Agda] ICFP 2021 Student Research Competition: Call for Submissions
Sam Tobin-Hochstadt
- [Agda] IFL'21 call for participation
Pieter Koopman
- [Agda] IFL'21 Final call for papers
Pieter Koopman
- [Agda] IFL'21 final call for participation
Pieter Koopman
- [Agda] IFL'21 Third call for papers
Pieter Koopman
- [Agda] IFL2021 second call for papers
Pieter Koopman
- [Agda] IJCAR 2022 - Call for Papers
Andrei Popescu
- [Agda] installing 2.6.2
mechvel at scico.botik.ru
- [Agda] installing 2.6.2
Orestis Melkonian
- [Agda] installing 2.6.2
Jesper Cockx
- [Agda] installing 2.6.2
mechvel at scico.botik.ru
- [Agda] installing 2.6.2
mechvel at scico.botik.ru
- [Agda] installing agda
Ingo Blechschmidt
- [Agda] installing agda
Nicolai Kraus
- [Agda] installing agda
Manuel Bärenz
- [Agda] installing agda
Ingo Blechschmidt
- [Agda] installing agda
Andrea Amantini
- [Agda] installing agda
Andrea Amantini
- [Agda] installing agda
Ingo Blechschmidt
- [Agda] installing agda
Andrea Amantini
- [Agda] installing agda
Gabriel Scherer
- [Agda] Is there currently a Problem with the standard lib from git?
stvienna wiener
- [Agda] Is there currently a Problem with the standard lib from git?
stvienna wiener
- [Agda] Journal of Functional Programming - Call for PhD Abstracts
Graham Hutton
- [Agda] Journal of Functional Programming - Call For PhD Abstracts
Graham Hutton
- [Agda] Lecturer in Verification position at University of Sheffield: deadline 29 March 2021
Andrei Popescu
- [Agda] lectures on Agda
selinger at mathstat.dal.ca
- [Agda] lectures on Agda
Jesper Cockx
- [Agda] lectures on Agda
Drazen Popovic
- [Agda] lectures on Agda
selinger at mathstat.dal.ca
- [Agda] level setting problem
mechvel at scico.botik.ru
- [Agda] level setting problem
Georgi Lyubenov
- [Agda] level setting problem
mechvel at scico.botik.ru
- [Agda] level setting problem
Georgi Lyubenov
- [Agda] level setting problem
Jesper Cockx
- [Agda] level setting problem
mechvel at scico.botik.ru
- [Agda] Looking for ESOP'22 AEC members
Andreea Costea
- [Agda] LOPSTR 2021 - Call for Papers: Extended Deadline
Niccolò Veltri
- [Agda] message for `,` without \prime
mechvel at scico.botik.ru
- [Agda] ML Family Workshop 2021: deadline extension
Jonathan Protzenko
- [Agda] ML Family Workshop 2021: deadline extension
Jonathan Protzenko
- [Agda] ML Family Workshop 2021: final call for short abstracts and presentations
Jonathan Protzenko
- [Agda] ML Family Workshop 2021: final call for short abstracts and presentations
Jonathan Protzenko
- [Agda] ML Family Workshop 2021: first call for short abstracts and presentations
Jonathan Protzenko
- [Agda] MSFP 2022 - Call for Papers
Max New
- [Agda] MSFP 2022 - First Call for Papers
Max New
- [Agda] multiple definitions in `let'
mechvel at scico.botik.ru
- [Agda] Need help completing a proof
Philip Wadler
- [Agda] Need help completing a proof
Miëtek Bak
- [Agda] Need help completing a proof
Conal Elliott
- [Agda] Need help completing a proof
Philip Wadler
- [Agda] Noetherian vs WellFounded
mechvel at scico.botik.ru
- [Agda] Noetherian vs WellFounded
Jason Hu
- [Agda] Noetherian vs WellFounded
mechvel at scico.botik.ru
- [Agda] Noetherian vs WellFounded
Martin Escardo
- [Agda] Noetherian vs WellFounded
mechvel at scico.botik.ru
- [Agda] Noetherian vs WellFounded
mechvel at scico.botik.ru
- [Agda] normalization question
Aaron Stump
- [Agda] normalization question
Jesper Cockx
- [Agda] normalization question
Martin Escardo
- [Agda] normalization question
Ulf Norell
- [Agda] normalization question
Aaron Stump
- [Agda] normalization question
Nils Anders Danielsson
- [Agda] normalization question
Aaron Stump
- [Agda] PEPM 2022 - First Call for Papers
Youyou Cong
- [Agda] PEPM 2022 - Second Call for Papers
Youyou Cong
- [Agda] PhD position in HoTT/UF at TU Delft
Benedikt Ahrens
- [Agda] PhD Position in Programming Languages at TU Delft
Casper Bach Poulsen
- [Agda] PhD position in Type Theory at Chalmers/Gothenburg University (deadline 8 Nov)
Andreas Abel
- [Agda] PhD position on program verification in Coq
David Nowak
- [Agda] PhD position on the formalization of logical calculi in Saarbrücken
Andrei Popescu
- [Agda] PhD Student Opportunity in the Granule Project
Harley D. Eades III
- [Agda] PLMW at POPL 2022: 2nd Call for Application
Robbert Krebbers
- [Agda] Poor man's way to latex Agda source
Eduardo Ochs
- [Agda] Poor man's way to latex Agda source
Jason Hu
- [Agda] Poor man's way to latex Agda source
Eduardo Ochs
- [Agda] Poor man's way to latex Agda source
Thorsten Altenkirch
- [Agda] Poor man's way to latex Agda source
Philip Wadler
- [Agda] Position of Lecturer or Senior Lecturer in Cybersecurity at University of Sheffield
Andrei Popescu
- [Agda] Postdoc position (7 months) on type theory, working remotely is possible
Benedikt Ahrens
- [Agda] Postdoctoral position in homotopy type theory and related topics at Stockholm University
Anders Mortberg
- [Agda] Postdoctoral position in HoTT
Thierry Coquand
- [Agda] Postdoctoral Research Assistant position at University of Edinburgh
Philip Wadler
- [Agda] Postdoctor in Modal operations for homotopy type theory
Ana Bove
- [Agda] PPDP 2021 Call for Papers
Niccolò Veltri
- [Agda] profiling
mechvel at scico.botik.ru
- [Agda] profiling
Ulf Norell
- [Agda] profiling
mechvel at scico.botik.ru
- [Agda] profiling
Ulf Norell
- [Agda] profiling
mechvel at scico.botik.ru
- [Agda] profiling
Ulf Norell
- [Agda] profiling
mechvel at scico.botik.ru
- [Agda] profiling
Ulf Norell
- [Agda] profiling
mechvel at scico.botik.ru
- [Agda] profiling
Ulf Norell
- [Agda] profiling
mechvel at scico.botik.ru
- [Agda] profiling
guillaume allais
- [Agda] Random number generator.
Serge Leblanc
- [Agda] Random number generator.
Serge Leblanc
- [Agda] Reminder: 2 year position on HoTT and related topics in Stockholm, deadline Friday next week
Anders Mortberg
- [Agda] Research internship Summer 2021 - Searching for verifiable neural network properties
Matthew Daggitt
- [Agda] Research position at fortiss, Munich
Chuangjie Xu
- [Agda] Research position in Formal Verification at HENSOLDT Cyber in Munich
Benedikt Ahrens
- [Agda] Research Programmer in HoTT and Cubical Type Theory
Favonia
- [Agda] School on Univalent Mathematics, Cortona (Italy), July 17-23, 2022
Marco Maggesi
- [Agda] Starting work on v2.0 of the Agda Standard Library
Matthew Daggitt
- [Agda] Submit to ITP 2021 (Interaction theorem proving): abstracts due 25 January
Andreas Abel
- [Agda] subst puzzle
Jacques Carette
- [Agda] subst puzzle
Paolo Capriotti
- [Agda] subst puzzle
Nils Anders Danielsson
- [Agda] subst puzzle
James Chapman
- [Agda] subst puzzle
Andreas Nuyts
- [Agda] subst puzzle
Jacques Carette
- [Agda] subst puzzle
Nils Anders Danielsson
- [Agda] subst puzzle
Jacques Carette
- [Agda] taking limit of a cumulative predicate
Jason Hu
- [Agda] taking limit of a cumulative predicate
Carette, Jacques
- [Agda] taking limit of a cumulative predicate
Jason Hu
- [Agda] Terminating checking for functions on induction-recursion
Jason Hu
- [Agda] Terminating checking for functions on induction-recursion
Jason Hu
- [Agda] termination checking & with
Robby Findler
- [Agda] Termination in algebraic encodings of families
John Paul Martin
- [Agda] Termination in algebraic encodings of families
Nils Anders Danielsson
- [Agda] test report
mechvel at scico.botik.ru
- [Agda] test report
Nils Anders Danielsson
- [Agda] test report
mechvel at scico.botik.ru
- [Agda] test report
mechvel at scico.botik.ru
- [Agda] test report
Nils Anders Danielsson
- [Agda] test report
mechvel at scico.botik.ru
- [Agda] test report
mechvel at scico.botik.ru
- [Agda] test report
Nils Anders Danielsson
- [Agda] test report
mechvel at scico.botik.ru
- [Agda] Tips for working around proof relevance
Daniel Lee
- [Agda] Tips for working around proof relevance
Sandro Stucki
- [Agda] two fully funded PhD positions in type theory
Thierry Coquand
- [Agda] TYPES 2021: Call for Contributions
Henning Basold
- [Agda] TYPES 2021: Call for Contributions (speakers and deadline extension)
Henning Basold
- [Agda] TYPES 2021: Call for Participation
Henning Basold
- [Agda] TYPES 2021 post-proceedings: Open call for papers
Henning Basold
- [Agda] TYPES 2021 post-proceedings: Second call for papers (Deadline extension)
Henning Basold
- [Agda] UPolyLight announce
mechvel at scico.botik.ru
- [Agda] Using Haskell randomRIO functions from Agda
Serge Leblanc
- [Agda] Using Haskell randomRIO functions from Agda
Nils Anders Danielsson
- [Agda] Vikraman Choudhury, Jacek Karwowski, Amr Sabry --- results to reversible circuits...formalisation ... HoTT-Agda library (around 7, 500 lines of code) ... accompanying Agda code
Art Scott
- [Agda] What does "Set !=< {some type}" mean?
David Banas
- [Agda] What does "Set !=< {some type}" mean?
Jesper Cockx
- [Agda] What does "Set !=< {some type}" mean?
James Wood
- [Agda] Which Agda with which GHC [Re: [ANNOUNCE] Agda 2.6.2 release candidate 2]
Andreas Abel
- [Agda] Which Agda with which GHC [Re: [ANNOUNCE] Agda 2.6.2 release candidate 2]
mechvel at scico.botik.ru
- [Agda] Which Agda with which GHC [Re: [ANNOUNCE] Agda 2.6.2 release candidate 2]
Andreas Abel
- [Agda] Why are some terms in the Agda goal report colored blue?
Nils Anders Danielsson
- [Agda] Why are some terms in the Agda goal report colored blue?
David Banas
- [Agda] Why are some terms in the Agda goal report colored blue?
Nils Anders Danielsson
- [Agda] Why are some terms in the Agda goal report colored blue?
James Wood
- [Agda] Why disallow case splits that involve impossible unification
James Smith
- [Agda] Why disallow case splits that involve impossible unification
Jason Hu
- [Agda] Why disallow case splits that involve impossible unification
James Wood
- [Agda] Why disallow case splits that involve impossible unification
James Smith
- [Agda] Why mutual is deprecated?
Jason -Zhong Sheng- Hu
- [Agda] Why mutual is deprecated?
Ulf Norell
- [Agda] WPTE 2021 (FIRST Call For Papers)
Keisuke Nakano
Last message date:
Wed Dec 29 12:27:50 CET 2021
Archived on: Wed Dec 29 12:28:12 CET 2021
This archive was generated by
Pipermail 0.09 (Mailman edition).