- May 2020 messages sorted by: [ thread ] [ subject ] [ author ]
- More info on this list...
- List archive Table of Contents

- Fri, 01 May 2020
- [isabelle] WFLP 2020 CFP (Workshop on Functional and Constraint Logic Programming) - Claudio Sacerdoti Coen, claudio.sacerdoticoen at unibo.it
- [isabelle] Non-idempotence of datatype constructors - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] Non-idempotence of datatype constructors - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] Non-idempotence of datatype constructors - Thomas Sewell, sewell at chalmers.se
- Re: [isabelle] Non-idempotence of datatype constructors - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors - Richard Waldinger, waldinger at AI.SRI.COM
- Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors - Miguel Pagano, miguel.pagano at gmail.com
- Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors - Miguel Pagano, miguel.pagano at gmail.com
- Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors - Manuel Eberl, eberlm at in.tum.de

- Sat, 02 May 2020
- Re: [isabelle] Non-idempotence of datatype constructors - Tobias Nipkow, nipkow at in.tum.de
- Re: [isabelle] Non-idempotence of datatype constructors - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] Non-idempotence of datatype constructors - Tobias Nipkow, nipkow at in.tum.de
- Re: [isabelle] Non-idempotence of datatype constructors - Manuel Eberl, eberlm at in.tum.de
- [isabelle] SMT 2020: Revised Call for Papers - Tjark Weber, tjark.weber at it.uu.se
- Re: [isabelle] Non-idempotence of datatype constructors - Manuel Eberl, eberlm at in.tum.de

- Sun, 03 May 2020
- [isabelle] ICFEM'20 deadline extended to 17th May 2020 - Jeremy Dawson, Jeremy.Dawson at anu.edu.au
- Re: [isabelle] Non-idempotence of datatype constructors - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] Non-idempotence of datatype constructors - Traytel Dmitriy, traytel at inf.ethz.ch

- Mon, 04 May 2020
- [isabelle] Final call for contributions for the virtual WiL 2020 (4th Women in Logic Worskhop collocated with Petri Nets, IJCAR etc) - Rozman, Mihaela, mihaela.rozman at tuwien.ac.at
- Re: [isabelle] Non-idempotence of datatype constructors - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] Non-idempotence of datatype constructors - Traytel Dmitriy, traytel at inf.ethz.ch

- Tue, 05 May 2020
- [isabelle] I launched a new project on Hackaday.io. It is in the use of the Isabelle HOL to verify and validate the DOOM source code from ID software. - David Blubaugh via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
- [isabelle] sledgehammer (or Z3) internal error - Lars-Henrik Eriksson, lhe at it.uu.se
- Re: [isabelle] sledgehammer (or Z3) internal error - Lars-Henrik Eriksson, lhe at it.uu.se

- Wed, 06 May 2020
- [isabelle] FMBC: Third Call for Papers - Marmsoler, Diego, D.Marmsoler at exeter.ac.uk
- [isabelle] A milestone for the AFP: Formalization of Forcing in Isabelle/ZF - Lawrence Paulson, lp15 at cam.ac.uk
- [isabelle] Also in the AFP: Banach-Steinhaus Theorem - Lawrence Paulson, lp15 at cam.ac.uk
- Re: [isabelle] Tiny minor backward-compatible changes to IFOL - Lawrence Paulson, lp15 at cam.ac.uk

- Thu, 07 May 2020
- Re: [isabelle] Non-idempotence of datatype constructors - Manuel Eberl, eberlm at in.tum.de
- [isabelle] Reification example fails to produce concrete representation - Albert Rizaldi, albert.rizaldi at ntu.edu.sg
- [isabelle] Strange eta-expanded "constants" in experiment environment - Peter Lammich, lammich at in.tum.de
- [isabelle] Prior work on proof assistant performance / optimization - Jason Gross, jasongross9 at gmail.com

- Fri, 08 May 2020
- [isabelle] Question about "isabelle scala" - Xingyuan Zhang, xingyuanzhang at 126.com
- Re: [isabelle] Prior work on proof assistant performance / optimization - Lawrence Paulson, lp15 at cam.ac.uk
- Re: [isabelle] Question about "isabelle scala" - Fernandez, Matthew, matthew.fernandez at intel.com

- Sat, 09 May 2020
- [isabelle] New in the AFP: An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] New AFP Feature: LaTeX formulae in abstracts - Makarius, makarius at sketis.net
- Re: [isabelle] New AFP Feature: LaTeX formulae in abstracts - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] New AFP Feature: LaTeX formulae in abstracts - Makarius, makarius at sketis.net
- [isabelle] New in the AFP: Matrices for ODEs - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] New AFP Feature: LaTeX formulae in abstracts - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] New AFP Feature: LaTeX formulae in abstracts - Makarius, makarius at sketis.net
- Re: [isabelle] Question about "isabelle scala" - Makarius, makarius at sketis.net
- Re: [isabelle] New AFP Feature: LaTeX formulae in abstracts - Pedro Sánchez Terraf, sterraf at famaf.unc.edu.ar

- Sun, 10 May 2020
- Re: [isabelle] Question about "isabelle scala" - Xingyuan Zhang, xingyuanzhang at 126.com

- Mon, 11 May 2020
- [isabelle] SMT 2020: Final Call for Papers - Tjark Weber, tjark.weber at it.uu.se
- [isabelle] 6-year PostDoc Position in Algorithms at the Vienna University of Technology (TU Wien), Vienna, Austria *** Application deadline is May 28, 2020 *** - Rozman, Mihaela, mihaela.rozman at tuwien.ac.at
- [isabelle] Proof Ground 2020 - Call for Problems - Max Haslbeck, haslbema at in.tum.de
- [isabelle] formal models of peripheral devices like GIC, NIC - Abhishek Anand, abhishek.anand.iitg at gmail.com

- Tue, 12 May 2020
- [isabelle] Several Open PhD Positions in the doctoral program on Logical Methods in Computer Science (LogiCS) in Austria ***Deadline: June 12, 2020*** - Rozman, Mihaela, mihaela.rozman at tuwien.ac.at
- Re: [isabelle] formal models of peripheral devices like GIC, NIC - Hira Taqdees Syeda, hira at chalmers.se
- Re: [isabelle] Bug in the algebra method for ideal membership - Makarius, makarius at sketis.net
- Re: [isabelle] Bug in the algebra method for ideal membership - Laurent Thery, Laurent.Thery at inria.fr
- Re: [isabelle] [Agda] [Coq-Club] Prior work on proof assistant performance / optimization - Wolfram Kahl, kahl at cas.mcmaster.ca

- Wed, 13 May 2020
- [isabelle] new in the AFP: Recursion Theorem in ZF - Lawrence Paulson, lp15 at cam.ac.uk
- Re: [isabelle] [EXTERNAL] new in the AFP: Recursion Theorem in ZF - Richard Waldinger, waldinger at AI.SRI.COM
- Re: [isabelle] [EXTERNAL] new in the AFP: Recursion Theorem in ZF - Richard Waldinger, waldinger at AI.SRI.COM
- [isabelle] New in the AFP: Irrationality Criteria for Series by Erdős and Straus - Thiemann, René, Rene.Thiemann at uibk.ac.at

- Thu, 14 May 2020
- Re: [isabelle] [Agda] Prior work on proof assistant performance / optimization - Jason Gross, jasongross9 at gmail.com
- Re: [isabelle] Prior work on proof assistant performance / optimization - Konrad Slind, konrad.slind at gmail.com

- Fri, 15 May 2020
- [isabelle] New in the AFP: A Formalization of Knuth–Bendix Orders - Tobias Nipkow, nipkow at in.tum.de
- [isabelle] Missing AFP entries after April 27 - Dr A. Koutsoukou-Argyraki, ak2110 at cam.ac.uk
- [isabelle] Fully funded PhD in Networking and Communication Technology at the University of Vienna, Austria ***Deadline: June 7, 2020*** - Rozman, Mihaela, mihaela.rozman at tuwien.ac.at

- Sat, 16 May 2020
- Re: [isabelle] Missing AFP entries after April 27 - Tobias Nipkow, nipkow at in.tum.de
- [isabelle] DOOM by Id Software... New Hackaday IO Project started that utilizes the DOOM source code to be verified and validated by the Isabelle HOL automated theorem prover. - David Blubaugh via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
- [isabelle] New in the AFP: A Formalization of Knuth–Bendix - Jens-D. Doll, jens.doll at live.de
- Re: [isabelle] New in the AFP: A Formalization of Knuth–Bendix - Thiemann, René, Rene.Thiemann at uibk.ac.at
- [isabelle] CfP: Workshop on Natural Formal Mathematics (NFM 2020) - Lawrence Paulson, lp15 at cam.ac.uk
- [isabelle] Workshop on Natural Formal Mathematics, part of CICM 2020 - Peter Koepke, koepke at math.uni-bonn.de

- Sun, 17 May 2020
- [isabelle] NBG in Isabelle/HOL? - Mikhail Chekhov, mikhail.chekhov.w at gmail.com
- Re: [isabelle] NBG in Isabelle/HOL? - Lawrence Paulson, lp15 at cam.ac.uk
- [isabelle] In a world of perfect interoperability between proof assistants, what tools would you combine? - Talia Ringer, tringer at cs.washington.edu

- Mon, 18 May 2020
- Re: [isabelle] [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine? - Klein, Gerwin (Data61, Kensington NSW), Gerwin.Klein at data61.csiro.au
- Re: [isabelle] [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine? - roux cody, cody.roux at gmail.com
- Re: [isabelle] [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine? - Talia Ringer, tringer at cs.washington.edu
- Re: [isabelle] NBG in Isabelle/HOL? - Joshua Chen, josh at joshchen.io
- [isabelle] New in the AFP: A Formalization of Knuth–Bendix - Jens-D. Doll, jens.doll at live.de
- Re: [isabelle] NBG in Isabelle/HOL? - Lawrence Paulson, lp15 at cam.ac.uk
- [isabelle] Tarski-Grothendieck set theory – Re: NBG in Isabelle/HOL? - Ken Kubota, mail at kenkubota.de
- [isabelle] FTfJP 2020 (virtual): Second CFP - Oortwijn Wytse, woortwijn at inf.ethz.ch
- Re: [isabelle] In a world of perfect interoperability between proof assistants, what tools would you combine? - Peter Lammich, lammich at in.tum.de
- Re: [isabelle] NBG in Isabelle/HOL? - Mikhail Chekhov, mikhail.chekhov.w at gmail.com
- [isabelle] Tarski-Grothendieck in Isabelle/HOL - Mikhail Chekhov, mikhail.chekhov.w at gmail.com

- Tue, 19 May 2020
- Re: [isabelle] New in the AFP: A Formalization of Knuth–Bendix - Thiemann, René, Rene.Thiemann at uibk.ac.at
- Re: [isabelle] [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine? - Mark Wassell, mpwassell at gmail.com
- [isabelle] Workshop on Logic Programming: Trends, Extensions, Applications, 28-29 May 2020 - Ekaterina Komendantskaya, komendantskaya at gmail.com
- [isabelle] ICFEM'20 - submission deadline extended - Jeremy Dawson, Jeremy.Dawson at anu.edu.au

- Wed, 20 May 2020
- [isabelle] new AFP entries - Klein, Gerwin (Data61, Kensington NSW), Gerwin.Klein at data61.csiro.au

- Sat, 23 May 2020
- [isabelle] Bit operations and word type - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
- [isabelle] Word authorship - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
- Re: [isabelle] Word authorship - Andreas Lochbihler, mail at andreas-lochbihler.de
- Re: [isabelle] Word authorship - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de

- Sun, 24 May 2020
- [isabelle] Research Positions in a project on AI Verification (Types, Programming Languages, Security, Machine Learning ) - Ekaterina Komendantskaya, komendantskaya at gmail.com

- Mon, 25 May 2020
- Re: [isabelle] Word authorship - Klein, Gerwin (Data61, Kensington NSW), Gerwin.Klein at data61.csiro.au
- [isabelle] New in the AFP: A verified algorithm for computing the Smith normal form of a matrix - Thiemann, René, Rene.Thiemann at uibk.ac.at
- Re: [isabelle] Reification example fails to produce concrete representation - Dominique Unruh, unruh at ut.ee

- Tue, 26 May 2020
- [isabelle] More on "References about mistakes and gaps in papers" - Andrei Popescu, andrei.h.popescu at gmail.com
- Re: [isabelle] More on "References about mistakes and gaps in papers" - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] More on "References about mistakes and gaps in papers" - Andrei Popescu, andrei.h.popescu at gmail.com
- [isabelle] Any fans of "try"? - Jasmin Blanchette via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
- Re: [isabelle] Any fans of "try"? - Peter Lammich, lammich at in.tum.de
- Re: [isabelle] Any fans of "try"? - Eugene W. Stark, isabelle-users at starkeffect.com
- Re: [isabelle] Any fans of "try"? - John F. Hughes, jfh at cs.brown.edu
- [isabelle] Isabelle Workshop 2020 - Makarius, makarius at sketis.net
- Re: [isabelle] Any fans of "try"? - Lawrence Paulson, lp15 at cam.ac.uk
- Re: [isabelle] Word authorship - Fernandez, Matthew, matthew.fernandez at intel.com
- Re: [isabelle] Any fans of "try"? - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] Any fans of "try"? - marco caminati via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
- [isabelle] AFP submission outage - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] Visualization of partial orders in Isabelle/HOL; use of external tools in the AFP entries - Mikhail Chekhov, mikhail.chekhov.w at gmail.com

- Thu, 28 May 2020
- [isabelle] linarith_split_limit_exceeded (current value is 9) - Dr A. Koutsoukou-Argyraki, ak2110 at cam.ac.uk

- Fri, 29 May 2020
- [isabelle] Thm.cterm_of does not check sort constraints - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] linarith_split_limit_exceeded (current value is 9) - Lawrence Paulson, lp15 at cam.ac.uk
- Re: [isabelle] linarith_split_limit_exceeded (current value is 9) - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] Thm.cterm_of does not check sort constraints - Makarius, makarius at sketis.net
- Re: [isabelle] linarith_split_limit_exceeded (current value is 9) - Peter Lammich, lammich at in.tum.de
- Re: [isabelle] [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine? - Abhishek Anand, abhishek.anand.iitg at gmail.com
- [isabelle] Retrieve overloadings of constant - Manuel Eberl, eberlm at in.tum.de
- Re: [isabelle] Retrieve overloadings of constant - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de