Cl-isabelle-users March 2021 Archives by subject

• March 2021 messages sorted by: [ thread ] [ author ] [ date ]
• More info on this list...
• List archive Table of Contents

• [isabelle] 14th Conference on Intelligent Computer Mathematics (CICM 2021) Final call for papers, Conference Date: July 26-31, 2021
  • Serge Autexier, serge.autexier at dfki.de - Tue, 16 Mar 2021 19:21:11 +0000
• [isabelle] 21st Midlands Graduate School in the Foundations of Computing Science: Final Call for Participation
  • Andrei Popescu, andrei.h.popescu at gmail.com - Wed, 17 Mar 2021 11:04:09 +0000
• [isabelle] 2nd CfP: SCSS 2021
  • Temur Kutsia, kutsia at risc.jku.at - Mon, 29 Mar 2021 14:47:08 +0100
• [isabelle] 7th International Workshop on Proof eXchange for Theorem Proving (PxTP) - First CFP
  • Chantal Keller, chantal.keller at wanadoo.fr - Tue, 09 Mar 2021 10:26:03 +0000
• [isabelle] A lemma about remove1
  • Jakub Kądziołka, kuba at kadziolka.net - Mon, 15 Mar 2021 13:37:03 +0000
  • Peter Lammich, lammich at in.tum.de - Mon, 15 Mar 2021 14:36:07 +0000
  • Tobias Nipkow, nipkow at in.tum.de - Tue, 16 Mar 2021 07:17:44 +0000
• [isabelle] Atb.: How to see the names of all active Isabelle sessions and how to export specific session?
  • Alex Meyer, alex153 at outlook.lv - Sat, 27 Mar 2021 14:21:39 +0000
• [isabelle] ATVA 2021 - Second Call for Papers
  • Giles Reger, giles.reger at manchester.ac.uk - Thu, 04 Mar 2021 16:50:52 +0000
• [isabelle] Bitblasting via SAT and Argo
  • Thomas Sewell, tals4 at cam.ac.uk - Fri, 05 Mar 2021 12:29:17 +0000
• [isabelle] building the document in Windows from Isabelle/jEdit
  • Stepan Holub, holub at karlin.mff.cuni.cz - Wed, 03 Mar 2021 18:10:16 +0000
  • Makarius, makarius at sketis.net - Mon, 15 Mar 2021 16:14:17 +0000
• [isabelle] build output
  • Tobias Nipkow, nipkow at in.tum.de - Mon, 01 Mar 2021 11:55:22 +0000
• [isabelle] by fact and try0
  • Stepan Holub, holub at karlin.mff.cuni.cz - Fri, 05 Mar 2021 12:34:48 +0000
  • Jasmin Blanchette via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Tue, 09 Mar 2021 16:37:52 +0000
• [isabelle] Call for Papers: HotSpot 2021
  • Toby Murray, toby.murray at unimelb.edu.au - Mon, 22 Mar 2021 06:43:08 +0000
• [isabelle] CFP ICTCS 2021 - 22th Italian Conference on Theoretical Computer Science
  • Claudio Sacerdoti Coen, claudio.sacerdoticoen at unibo.it - Thu, 25 Mar 2021 20:13:49 +0000
• [isabelle] [CFP] Logical Frameworks and Meta-Languages: Theory and Practice
  • Enrico Tassi, Enrico.Tassi at inria.fr - Mon, 15 Mar 2021 08:23:38 +0000
• [isabelle] Code generation for a subtype with free_constructors
  • Lukas Stevens, lukas.stevens+isabelle-users at in.tum.de - Tue, 02 Mar 2021 11:55:05 +0000
• [isabelle] Concerning Fun.swap
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Sun, 28 Mar 2021 10:20:46 +0100
  • Lawrence Paulson, lp15 at cam.ac.uk - Sun, 28 Mar 2021 15:34:04 +0100
• [isabelle] C-to-Isabelle multiple external files
  • Adriana Stancu, adriana.stancu95 at gmail.com - Sun, 21 Mar 2021 08:36:45 +0000
  • Thomas Sewell, tals4 at cam.ac.uk - Mon, 22 Mar 2021 10:40:40 +0000
  • Yakoub Nemouchi, y.nemouchi at gmail.com - Mon, 22 Mar 2021 10:53:59 +0000
  • Jaap Boender, jaapb at kerguelen.org - Tue, 23 Mar 2021 10:19:59 +0000
• [isabelle] Deadline Extension: April 5th, 20201, 14th Conference on Intelligent Computer Mathematics (CICM 2021)
  • Serge Autexier, serge.autexier at dfki.de - Mon, 29 Mar 2021 19:45:47 +0100
• [isabelle] Entire theory in JSON forma using scala-isabelle?
  • Alex Meyer, alex153 at outlook.lv - Sun, 14 Mar 2021 16:38:56 +0000
  • Dominique Unruh, unruh at ut.ee - Mon, 15 Mar 2021 11:50:16 +0000
  • Makarius, makarius at sketis.net - Mon, 15 Mar 2021 12:17:01 +0000
• Re: [isabelle] Error in DockerHub documentation
  • Boris Shminke via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Mon, 01 Mar 2021 11:59:29 +0000
  • Makarius, makarius at sketis.net - Mon, 01 Mar 2021 14:08:46 +0000
• [isabelle] Evaluation of definitions defined inside a locale
  • Sanan Baena David Miguel (Dr), sanan at ntu.edu.sg - Thu, 25 Mar 2021 08:22:48 +0000
  • Thiemann, René, Rene.Thiemann at uibk.ac.at - Sun, 28 Mar 2021 18:41:26 +0100
  • Sanan Baena David Miguel (Dr), sanan at ntu.edu.sg - Wed, 31 Mar 2021 05:57:03 +0100
  • YAMADA, Akihisa, ayamada at trs.cm.is.nagoya-u.ac.jp - Wed, 31 Mar 2021 06:17:39 +0100
  • Sanan Baena David Miguel (Dr), sanan at ntu.edu.sg - Wed, 31 Mar 2021 06:54:29 +0100
• [isabelle] Fixing type variables in locales
  • Wolfgang Jeltsch, wolfgang-it at jeltsch.info - Tue, 02 Mar 2021 13:23:34 +0000
  • Christian Sternagel, c.sternagel at gmail.com - Tue, 02 Mar 2021 13:35:57 +0000
  • Thiemann, René, Rene.Thiemann at uibk.ac.at - Tue, 02 Mar 2021 14:00:14 +0000
  • Wolfgang Jeltsch, wolfgang-it at jeltsch.info - Tue, 02 Mar 2021 14:34:17 +0000
  • Makarius, makarius at sketis.net - Wed, 03 Mar 2021 11:15:31 +0000
  • Wolfgang Jeltsch, wolfgang-it at jeltsch.info - Wed, 03 Mar 2021 14:13:42 +0000
• [isabelle] Formal algorithms in Isabelle - is it OK to specify algorithm as definition or is specification as function required?
  • Alex Meyer, alex153 at outlook.lv - Sat, 20 Mar 2021 19:00:18 +0000
  • Jakub Kądziołka, kuba at kadziolka.net - Sat, 20 Mar 2021 19:46:21 +0000
• [isabelle] hd and last of Nil
  • Stepan Holub, holub at karlin.mff.cuni.cz - Wed, 24 Mar 2021 20:30:15 +0000
  • Lawrence Paulson, lp15 at cam.ac.uk - Wed, 24 Mar 2021 21:32:30 +0000
  • Manuel Eberl, eberlm at in.tum.de - Wed, 24 Mar 2021 21:46:21 +0000
  • Stepan Holub, holub at karlin.mff.cuni.cz - Thu, 25 Mar 2021 07:25:14 +0000
  • Tjark Weber, tjark.weber at it.uu.se - Thu, 25 Mar 2021 10:23:21 +0000
  • Manuel Eberl, eberlm at in.tum.de - Thu, 25 Mar 2021 15:23:20 +0000
  • Jeremy Dawson, Jeremy.Dawson at anu.edu.au - Thu, 25 Mar 2021 22:55:58 +0000
  • John F. Hughes, jfh at cs.brown.edu - Thu, 25 Mar 2021 23:15:19 +0000
  • Mario Carneiro, di.gama at gmail.com - Thu, 25 Mar 2021 23:34:15 +0000
  • Norrish, Michael (Data61, Acton), Michael.Norrish at data61.csiro.au - Thu, 25 Mar 2021 23:35:17 +0000
  • Tjark Weber, tjark.weber at it.uu.se - Fri, 26 Mar 2021 11:01:06 +0000
  • Thomas Sewell, tals4 at cam.ac.uk - Fri, 26 Mar 2021 11:09:10 +0000
  • Kevin Kappelmann, kevin.kappelmann at tum.de - Fri, 26 Mar 2021 11:19:17 +0000
  • Stepan Holub, holub at karlin.mff.cuni.cz - Fri, 26 Mar 2021 14:21:37 +0000
  • Thomas Sewell, tals4 at cam.ac.uk - Mon, 29 Mar 2021 12:36:32 +0100
• [isabelle] How to see the names of all active Isabelle sessions and how to export specific session?
  • Alex Meyer, alex153 at outlook.lv - Mon, 22 Mar 2021 15:39:29 +0000
• Re: [isabelle] How to see the names of all active Isabelle sessions and how to export specific session?
  • Jakub Kądziołka, kuba at kadziolka.net - Mon, 22 Mar 2021 15:42:15 +0000
• [isabelle] I completed mmt_import but now I have some questions
  • Alex Meyer, alex153 at outlook.lv - Sun, 28 Mar 2021 02:26:59 +0100
  • Makarius, makarius at sketis.net - Sun, 28 Mar 2021 14:35:21 +0100
• [isabelle] Isabelle 2021 Word Library
  • Freek Verbeek, freek at vt.edu - Thu, 04 Mar 2021 11:15:16 +0000
  • Peter Lammich, lammich at in.tum.de - Fri, 05 Mar 2021 10:09:55 +0000
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Fri, 05 Mar 2021 11:11:45 +0000
• [isabelle] \isakeyword in bold?
  • Tobias Nipkow, nipkow at in.tum.de - Thu, 18 Mar 2021 10:15:35 +0000
• [isabelle] Pārs.: Entire theory in JSON forma using scala-isabelle?
  • Alex Meyer, alex153 at outlook.lv - Sun, 14 Mar 2021 16:54:32 +0000
• [isabelle] keywords "spark_open" :: thy_load (spark_siv)
  • Walther Neuper, walther.neuper at jku.at - Mon, 08 Mar 2021 13:36:01 +0000
  • Makarius, makarius at sketis.net - Mon, 08 Mar 2021 18:56:09 +0000
  • Walther Neuper, walther.neuper at jku.at - Wed, 10 Mar 2021 17:21:56 +0000
  • Makarius, makarius at sketis.net - Wed, 10 Mar 2021 17:33:24 +0000
  • Walther Neuper, walther.neuper at jku.at - Fri, 12 Mar 2021 16:17:15 +0000
  • Makarius, makarius at sketis.net - Fri, 12 Mar 2021 16:28:09 +0000
• [isabelle] Lecturer in Verification position at University of Sheffield: deadline 29 March 2021
  • Andrei Popescu, andrei.h.popescu at gmail.com - Sat, 13 Mar 2021 01:23:07 +0000
• [isabelle] ML questions
  • Jaap Boender, jaapb at kerguelen.org - Thu, 11 Mar 2021 07:46:44 +0000
  • Thomas Sewell, tals4 at cam.ac.uk - Sat, 13 Mar 2021 10:25:52 +0000
  • Peter Lammich, lammich at in.tum.de - Sat, 13 Mar 2021 11:16:42 +0000
• [isabelle] Morello: Edinburgh research posts on capability-based security technologies
  • Ian Stark, Ian.Stark at ed.ac.uk - Sun, 28 Mar 2021 18:51:16 +0100
• [isabelle] New in the AFP: Constructive Cryptography in HOL: the Communication Modeling Aspect
  • Thiemann, René, Rene.Thiemann at uibk.ac.at - Thu, 18 Mar 2021 07:51:37 +0000
• [isabelle] New in the AFP: Mereology
  • Tobias Nipkow, nipkow at in.tum.de - Fri, 05 Mar 2021 12:09:26 +0000
• [isabelle] New in the AFP: Quantum projective measurements
  • Lawrence Paulson, lp15 at cam.ac.uk - Tue, 09 Mar 2021 15:00:27 +0000
• [isabelle] New in the AFP: Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
  • Andreas Lochbihler, mail at andreas-lochbihler.de - Sun, 14 Mar 2021 11:13:09 +0000
• [isabelle] Nitpick finds counterexample to proven lemma
  • Sander van Rijnswou, svanrijnswou at gmail.com - Tue, 02 Mar 2021 14:35:19 +0000
  • Stepan Holub, holub at karlin.mff.cuni.cz - Sat, 06 Mar 2021 09:00:27 +0000
• [isabelle] Possible problem with floating-point addition in Approximation etc.
  • Manuel Eberl, eberlm at in.tum.de - Wed, 24 Mar 2021 16:46:41 +0000
  • Manuel Eberl, eberlm at in.tum.de - Wed, 24 Mar 2021 17:10:52 +0000
  • Fabian Immler via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Fri, 26 Mar 2021 12:37:28 +0000
• [isabelle] Proof Ground 2021 - Call for Problems
  • Maximilian Haslbeck, haslbema at in.tum.de - Mon, 29 Mar 2021 10:17:15 +0100
• Re: [isabelle] Python client to Isabelle server
  • Makarius, makarius at sketis.net - Mon, 01 Mar 2021 13:29:06 +0000
  • Boris Shminke via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Tue, 02 Mar 2021 13:58:45 +0000
  • Makarius, makarius at sketis.net - Thu, 04 Mar 2021 22:29:46 +0000
• Re: [isabelle] Remaining uses of "isabelle process" and "isabelle console"
  • Dominique Unruh, unruh at ut.ee - Mon, 01 Mar 2021 11:25:59 +0000
  • Makarius, makarius at sketis.net - Mon, 01 Mar 2021 12:45:15 +0000
  • Dominique Unruh, unruh at ut.ee - Mon, 08 Mar 2021 10:25:33 +0000
  • Makarius, makarius at sketis.net - Mon, 08 Mar 2021 11:49:16 +0000
  • Makarius, makarius at sketis.net - Mon, 08 Mar 2021 12:41:04 +0000
  • Dominique Unruh, unruh at ut.ee - Wed, 17 Mar 2021 12:58:29 +0000
  • Makarius, makarius at sketis.net - Wed, 17 Mar 2021 14:27:05 +0000
  • Makarius, makarius at sketis.net - Wed, 17 Mar 2021 15:03:24 +0000
• [isabelle] Request for feedback: dedicated session or AFP entry for material on combinatorics?
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Thu, 11 Mar 2021 11:03:46 +0000
• Re: [isabelle] Request for feedback: dedicated session or AFP entry for material on combinatorics?
  • Lawrence Paulson, lp15 at cam.ac.uk - Thu, 11 Mar 2021 11:18:36 +0000
  • Manuel Eberl, eberlm at in.tum.de - Thu, 11 Mar 2021 11:41:20 +0000
  • Tobias Nipkow, nipkow at in.tum.de - Thu, 11 Mar 2021 19:06:33 +0000
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Sat, 13 Mar 2021 07:30:27 +0000
  • Tobias Nipkow, nipkow at in.tum.de - Sat, 13 Mar 2021 13:46:18 +0000
• [isabelle] Research Programmer in HoTT and Cubical Type Theory
  • Favonia via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Sat, 13 Mar 2021 01:15:41 +0000
• Re: [isabelle] Some more polishing of the multiset theory
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Thu, 11 Mar 2021 10:46:38 +0000
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Thu, 11 Mar 2021 10:49:50 +0000
• [isabelle] Specifying a Universal Property in a locale definition
  • AARON CRIGHTON, crightoa at mcmaster.ca - Mon, 15 Mar 2021 19:35:40 +0000
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Mon, 22 Mar 2021 06:11:14 +0000
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Tue, 23 Mar 2021 19:42:49 +0000
• [isabelle] SPIN 2021 - Deadline extension to April 20
  • Laarman, A.W., a.w.laarman at liacs.leidenuniv.nl - Wed, 03 Mar 2021 15:02:13 +0000
• [isabelle] Structure of Proofs
  • Jens-D. Doll, jens.doll at live.de - Sun, 07 Mar 2021 11:01:08 +0000
  • Dr A. Koutsoukou-Argyraki, ak2110 at cam.ac.uk - Sun, 07 Mar 2021 18:26:54 +0000
  • Jens-D. Doll, jens.doll at live.de - Mon, 08 Mar 2021 17:17:25 +0000
• [isabelle] Towards a formalization of elements of the foundations of category theory in ZFC in HOL
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Wed, 03 Mar 2021 20:13:24 +0000
• [isabelle] Troubles building Pure; can't find Foreign.buildCall3
  • Jakub Kądziołka, kuba at kadziolka.net - Sat, 06 Mar 2021 00:30:30 +0000
  • Jakub Kądziołka, kuba at kadziolka.net - Sat, 06 Mar 2021 23:15:41 +0000
• [isabelle] New in the AFP: The Hermite–Lindemann–Weierstraß Transcendence Theorem
  • Lawrence Paulson, lp15 at cam.ac.uk - Fri, 12 Mar 2021 14:37:46 +0000
• [isabelle] New in the AFP: The Sunflower Lemma of Erdős and Rado
  • Tobias Nipkow, nipkow at in.tum.de - Mon, 01 Mar 2021 12:37:07 +0000
• [isabelle] Pārs.: How to see the names of all active Isabelle sessions and how to export specific session?
  • Alex Meyer, alex153 at outlook.lv - Sat, 27 Mar 2021 14:41:21 +0000
• [isabelle] Working with list symmetry (Attributes for theory-specific theorem transformations?)
  • Martin Raška, RaskaMartin at seznam.cz - Tue, 02 Mar 2021 08:58:52 +0000
• [isabelle] VS Code extension
  • Jeremy Sylvestre, jsylvest at ualberta.ca - Tue, 02 Mar 2021 06:53:08 +0000
  • Makarius, makarius at sketis.net - Tue, 02 Mar 2021 09:58:28 +0000
  • Jeremy Sylvestre, jsylvest at ualberta.ca - Tue, 02 Mar 2021 17:33:38 +0000
  • Jeremy Sylvestre, jsylvest at ualberta.ca - Tue, 02 Mar 2021 17:52:57 +0000
• [isabelle] Weak lemma: sum_mset_diff
  • Jakub Kądziołka, kuba at kadziolka.net - Sun, 21 Mar 2021 22:25:32 +0000
• [isabelle] Well-behaved MacOS application for Isabelle 2021
  • Frédéric Boulanger, frederic.boulanger at lri.fr - Thu, 11 Mar 2021 17:26:06 +0000