Cl-isabelle-users February 2021 Archives by subject

• February 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), Invited Speakers Update & Second call for papers, Conference Date: July 26-31, 2021
  • Serge Autexier, serge.autexier at dfki.de - Sat, 20 Feb 2021 16:09:54 +0000
• [isabelle] 21st Midlands Graduate School in the Foundations of Computing Science: Call for Participation
  • Andrei Popescu, andrei.h.popescu at gmail.com - Tue, 09 Feb 2021 16:40:23 +0000
• [isabelle] 2nd CfP ThEdu'21
  • Walther Neuper, walther.neuper at jku.at - Fri, 19 Feb 2021 17:34:56 +0000
• [isabelle] AFP 2021
  • Gerwin Klein, kleing at unsw.edu.au - Tue, 23 Feb 2021 10:19:22 +0000
  • Makarius, makarius at sketis.net - Tue, 23 Feb 2021 11:55:31 +0000
• [isabelle] AFP instructions
  • Stepan Holub, holub at karlin.mff.cuni.cz - Wed, 24 Feb 2021 16:40:20 +0000
  • Makarius, makarius at sketis.net - Wed, 24 Feb 2021 18:38:04 +0000
  • Stepan Holub, holub at karlin.mff.cuni.cz - Wed, 24 Feb 2021 18:47:19 +0000
  • Gerwin Klein, kleing at unsw.edu.au - Wed, 24 Feb 2021 22:14:36 +0000
  • Fernandez, Matthew, matthew.fernandez at intel.com - Wed, 24 Feb 2021 23:07:25 +0000
  • Gerwin Klein, kleing at unsw.edu.au - Wed, 24 Feb 2021 23:47:28 +0000
  • Stepan Holub, holub at karlin.mff.cuni.cz - Thu, 25 Feb 2021 08:03:11 +0000
  • Gerwin Klein, kleing at unsw.edu.au - Thu, 25 Feb 2021 09:47:39 +0000
  • Makarius, makarius at sketis.net - Thu, 25 Feb 2021 11:20:08 +0000
  • Makarius, makarius at sketis.net - Thu, 25 Feb 2021 11:25:07 +0000
  • Fernandez, Matthew, matthew.fernandez at intel.com - Thu, 25 Feb 2021 19:07:05 +0000
  • David Cock, david.cock at inf.ethz.ch - Thu, 25 Feb 2021 21:41:36 +0000
  • Gerwin Klein, kleing at unsw.edu.au - Thu, 25 Feb 2021 21:59:53 +0000
  • Gerwin Klein, kleing at unsw.edu.au - Fri, 26 Feb 2021 05:44:17 +0000
  • Stepan Holub, holub at karlin.mff.cuni.cz - Sat, 27 Feb 2021 09:28:26 +0000
  • Makarius, makarius at sketis.net - Sat, 27 Feb 2021 11:18:18 +0000
  • Makarius, makarius at sketis.net - Sat, 27 Feb 2021 11:34:39 +0000
  • Stepan Holub, holub at karlin.mff.cuni.cz - Sat, 27 Feb 2021 12:00:09 +0000
  • Makarius, makarius at sketis.net - Sat, 27 Feb 2021 12:29:20 +0000
  • Gerwin Klein, kleing at unsw.edu.au - Sun, 28 Feb 2021 21:24:44 +0000
• [isabelle] Announcing Isabelle2021
  • Makarius, makarius at sketis.net - Sun, 21 Feb 2021 20:50:19 +0000
• [isabelle] Assistant/Associate Professor positions in Edinburgh, UK (Herio-Watt University): Logic, Programming Languages, Verification, Security
  • Ekaterina Komendantskaya, komendantskaya at gmail.com - Tue, 16 Feb 2021 13:33:36 +0000
• [isabelle] Atb.: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories)
  • Alex Meyer, alex153 at outlook.lv - Fri, 05 Feb 2021 22:38:39 +0000
• [isabelle] Berghofer's program extraction mechanism and code generation
  • Dr A. Koutsoukou-Argyraki, ak2110 at cam.ac.uk - Tue, 23 Feb 2021 17:56:56 +0000
  • Manuel Eberl, eberlm at in.tum.de - Tue, 23 Feb 2021 18:09:04 +0000
  • Tjark Weber, tjark.weber at it.uu.se - Wed, 24 Feb 2021 00:59:32 +0000
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Thu, 25 Feb 2021 15:55:24 +0000
• [isabelle] Bill McCune PhD Award in Automated Reasoning, Call for Nominations
  • Pascal Fontaine, Pascal.Fontaine at inria.fr - Wed, 24 Feb 2021 13:14:56 +0000
• [isabelle] Boolos's Curious Inference (Speed-Up) in Isabelle/HOL
  • Jeffrey Ketland, jeffreyketland at gmail.com - Wed, 10 Feb 2021 02:20:53 +0000
  • Jakub Kądziołka, kuba at kadziolka.net - Wed, 10 Feb 2021 13:40:24 +0000
• [isabelle] Call for Papers: Tests and Proofs 2021 (TAP 2021) New Deadlines
  • Frederic Loulergue, frederic.loulergue at univ-orleans.fr - Tue, 02 Feb 2021 06:57:50 +0000
• [isabelle] CFP SAT-2021: Deadline March 19th
  • Jesús Giráldez Crú, jgiraldez at ugr.es - Thu, 11 Feb 2021 14:10:48 +0000
• [isabelle] CfP: SCSS 2021
  • Temur Kutsia, kutsia at risc.jku.at - Tue, 02 Feb 2021 11:21:15 +0000
• [isabelle] Comparing Isabelle/Scala with scala-isabelle. Was: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories)
  • Dominique Unruh, unruh at ut.ee - Tue, 09 Feb 2021 18:34:56 +0000
  • Makarius, makarius at sketis.net - Tue, 09 Feb 2021 19:33:31 +0000
  • Makarius, makarius at sketis.net - Tue, 09 Feb 2021 20:19:27 +0000
  • Dominique Unruh, unruh at ut.ee - Thu, 11 Feb 2021 11:54:42 +0000
  • Makarius, makarius at sketis.net - Thu, 11 Feb 2021 13:22:22 +0000
• [isabelle] Conflict of type arities: What are the constraints on class instantiations?
  • Peter Lammich, lammich at in.tum.de - Tue, 16 Feb 2021 12:52:28 +0000
• Re: [isabelle] Conflict of type arities: What are the constraints on class instantiations?
  • Tobias Nipkow, nipkow at in.tum.de - Tue, 16 Feb 2021 13:04:41 +0000
  • Jakub Kądziołka, kuba at kadziolka.net - Tue, 16 Feb 2021 14:56:10 +0000
  • Jeremy Dawson, Jeremy.Dawson at anu.edu.au - Wed, 17 Feb 2021 00:48:06 +0000
• [isabelle] Error in DockerHub documentation
  • Boris Shminke via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Wed, 24 Feb 2021 10:33:07 +0000
  • Makarius, makarius at sketis.net - Wed, 24 Feb 2021 18:01:09 +0000
  • Boris Shminke via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Wed, 24 Feb 2021 19:37:51 +0000
  • Makarius, makarius at sketis.net - Wed, 24 Feb 2021 19:52:45 +0000
  • Boris Shminke via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Thu, 25 Feb 2021 09:18:22 +0000
  • Makarius, makarius at sketis.net - Sun, 28 Feb 2021 11:00:01 +0000
• [isabelle] F-IDE 2021 - Last Call for Papers - Extended Deadline
  • Andrei Paskevich, andrei.paskevich at lri.fr - Wed, 24 Feb 2021 20:28:38 +0000
• [isabelle] First day with HOL/Isabelle
  • McCue, Brian, brian.mccue at snhu.edu - Sat, 20 Feb 2021 17:24:17 +0000
  • C. Diekmann, diekmann at in.tum.de - Sun, 21 Feb 2021 15:49:29 +0000
  • Jakub Kądziołka, kuba at kadziolka.net - Sun, 21 Feb 2021 18:29:07 +0000
  • Thomas Sewell, tals4 at cam.ac.uk - Sun, 21 Feb 2021 20:03:49 +0000
• [isabelle] FMBC 2021: First Call for Papers
  • Marmsoler, Diego, D.Marmsoler at exeter.ac.uk - Sat, 27 Feb 2021 14:17:31 +0000
• [isabelle] FMCAD 2021: First Call for Papers
  • Michael Whalen via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Thu, 25 Feb 2021 15:04:47 +0000
• [isabelle] FSCD 2021: Extended deadline (Abstract: February 16/ Submission: February 22)
  • Carsten Fuhs, carsten at dcs.bbk.ac.uk - Thu, 11 Feb 2021 09:06:41 +0000
• [isabelle] Incompatibility between code generation, HOL-Library.Numeral_Type, and Containers.Set_Impl
  • Dominique Unruh, unruh at ut.ee - Fri, 05 Feb 2021 13:20:59 +0000
• Re: [isabelle] Isabelle2021-RC0: Java/VM monitor
  • Makarius, makarius at sketis.net - Mon, 01 Feb 2021 15:11:51 +0000
  • Eugene W. Stark, isabelle-users at starkeffect.com - Mon, 01 Feb 2021 15:33:49 +0000
• Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use?
  • Jasmin Blanchette via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Thu, 04 Feb 2021 08:09:24 +0000
  • Dominique Unruh, unruh at ut.ee - Thu, 04 Feb 2021 10:20:56 +0000
  • Makarius, makarius at sketis.net - Fri, 05 Feb 2021 13:35:56 +0000
• Re: [isabelle] Isabelle2021-RC2: slight regression in HTML output
  • Makarius, makarius at sketis.net - Mon, 01 Feb 2021 14:58:59 +0000
• Re: [isabelle] Isabelle2021-RC3: Java 11 (LTS) vs. Java 15 (MTS)
  • Makarius, makarius at sketis.net - Mon, 01 Feb 2021 15:09:41 +0000
• Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer
  • Eugene W. Stark, isabelle-users at starkeffect.com - Sat, 13 Feb 2021 16:20:25 +0000
  • Mathias Fleury, mathias.fleury12 at gmail.com - Tue, 16 Feb 2021 07:26:57 +0000
  • Makarius, makarius at sketis.net - Tue, 16 Feb 2021 10:18:24 +0000
  • Eugene W. Stark, isabelle-users at starkeffect.com - Tue, 16 Feb 2021 12:19:16 +0000
  • Mathias Fleury, mathias.fleury12 at gmail.com - Tue, 16 Feb 2021 13:30:14 +0000
• [isabelle] Isabelle2021-RC4 available for applications
  • Makarius, makarius at sketis.net - Mon, 01 Feb 2021 14:45:46 +0000
• Re: [isabelle] Isabelle2021-RC4: bundling of Naproche-SAD
  • Makarius, makarius at sketis.net - Mon, 01 Feb 2021 14:51:13 +0000
• [isabelle] Isabelle2021-RC5 available for applications
  • Makarius, makarius at sketis.net - Mon, 08 Feb 2021 21:42:36 +0000
• Re: [isabelle] Isabelle2021-RC5: support for Apple Silicon
  • Makarius, makarius at sketis.net - Mon, 08 Feb 2021 22:09:13 +0000
  • Makarius, makarius at sketis.net - Sat, 13 Feb 2021 12:57:04 +0000
• [isabelle] Isabelle2021-RC6 available for applications
  • Makarius, makarius at sketis.net - Sun, 14 Feb 2021 18:42:54 +0000
• Re: [isabelle] Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories)
  • Makarius, makarius at sketis.net - Wed, 03 Feb 2021 12:58:23 +0000
  • Wenda Li, wl302 at cam.ac.uk - Fri, 05 Feb 2021 19:39:36 +0000
  • Makarius, makarius at sketis.net - Fri, 05 Feb 2021 19:58:09 +0000
  • Wenda Li, wl302 at cam.ac.uk - Fri, 05 Feb 2021 20:56:36 +0000
• [isabelle] Isabelle logo terms of use
  • Stepan Holub, holub at karlin.mff.cuni.cz - Mon, 01 Feb 2021 19:27:17 +0000
  • Makarius, makarius at sketis.net - Tue, 02 Feb 2021 19:54:58 +0000
• Re: [isabelle] isabelle scala_project and Gradle / IntelliJ support
  • Makarius, makarius at sketis.net - Thu, 11 Feb 2021 13:44:13 +0000
• [isabelle] New in the AFP: a port of GeoCoq
  • Lawrence Paulson, lp15 at cam.ac.uk - Mon, 01 Feb 2021 12:05:07 +0000
• [isabelle] New in the AFP: A Verified Imperative Implementation of B-Trees
  • Gerwin Klein, kleing at unsw.edu.au - Fri, 26 Feb 2021 06:26:54 +0000
• [isabelle] New in the AFP: Formal Puiseux Series
  • Lawrence Paulson, lp15 at cam.ac.uk - Wed, 24 Feb 2021 14:17:54 +0000
  • Manuel Eberl, eberlm at in.tum.de - Wed, 24 Feb 2021 14:59:51 +0000
  • Wenda Li, wl302 at cam.ac.uk - Wed, 24 Feb 2021 16:10:24 +0000
  • Manuel Eberl, eberlm at in.tum.de - Wed, 24 Feb 2021 16:15:19 +0000
  • Freek Wiedijk, freek at cs.ru.nl - Wed, 24 Feb 2021 16:39:02 +0000
  • Manuel Eberl, eberlm at in.tum.de - Fri, 26 Feb 2021 15:42:48 +0000
  • Manuel Eberl, eberlm at in.tum.de - Fri, 26 Feb 2021 15:51:42 +0000
  • Mohammad Abdulaziz, mohammad.abdulaziz8 at gmail.com - Fri, 26 Feb 2021 16:06:14 +0000
  • Manuel Eberl, eberlm at in.tum.de - Fri, 26 Feb 2021 16:15:52 +0000
  • Manuel Eberl, eberlm at in.tum.de - Fri, 26 Feb 2021 16:26:51 +0000
  • Mohammad Abdulaziz, mohammad.abdulaziz8 at gmail.com - Fri, 26 Feb 2021 16:27:04 +0000
  • Freek Wiedijk, freek at cs.ru.nl - Fri, 26 Feb 2021 16:28:47 +0000
• [isabelle] New in the AFP: Solution to the xkcd Blue Eyes puzzle
  • Manuel Eberl, eberlm at in.tum.de - Mon, 01 Feb 2021 17:24:18 +0000
• [isabelle] New in the AFP: The Laws of Large Numbers
  • Gerwin Klein, kleing at unsw.edu.au - Thu, 11 Feb 2021 05:40:33 +0000
• [isabelle] Nitpick Codatatype - No Counterexample found
  • Stüber, Sebastian, stueber at se-rwth.de - Fri, 26 Feb 2021 10:36:24 +0000
• [isabelle] Open pdf files from Isabelle File Browser
  • Peter Koepke, koepke at math.uni-bonn.de - Tue, 16 Feb 2021 07:17:46 +0000
  • Makarius, makarius at sketis.net - Tue, 16 Feb 2021 09:56:10 +0000
• [isabelle] PhD position in Formal Methods/Decompilation at the Open University of The Netherlands
  • Freek Verbeek, freek at vt.edu - Thu, 11 Feb 2021 10:08:39 +0000
• [isabelle] Postdoc/phd positions in ERC project "Certified Quantum Security" (formal verification of quantum crypto)
  • Dominique Unruh, unruh at ut.ee - Thu, 25 Feb 2021 12:43:10 +0000
• [isabelle] Predicate Compiler fails with "No specification for ..."
  • Florian Märkl, isabelle-users at florianmaerkl.de - Fri, 19 Feb 2021 14:03:51 +0000
• Re: [isabelle] Predicate Compiler fails with "No specification for ..."
  • Tobias Nipkow, nipkow at in.tum.de - Sat, 20 Feb 2021 17:07:56 +0000
  • Florian Märkl, isabelle-users at florianmaerkl.de - Sat, 20 Feb 2021 18:32:20 +0000
  • Andreas Lochbihler, mail at andreas-lochbihler.de - Sun, 21 Feb 2021 08:10:14 +0000
  • Florian Märkl, isabelle-users at florianmaerkl.de - Sun, 21 Feb 2021 16:34:11 +0000
  • Andreas Lochbihler, mail at andreas-lochbihler.de - Sun, 21 Feb 2021 19:20:38 +0000
• [isabelle] Python client to Isabelle server
  • Boris Shminke via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Fri, 26 Feb 2021 15:56:23 +0000
• [isabelle] RC5: Short experience report
  • Peter Lammich, lammich at in.tum.de - Fri, 12 Feb 2021 18:29:34 +0000
  • Jasmin Blanchette via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Mon, 15 Feb 2021 09:16:29 +0000
  • Lawrence Paulson, lp15 at cam.ac.uk - Mon, 15 Feb 2021 12:19:59 +0000
  • Tobias Nipkow, nipkow at in.tum.de - Mon, 15 Feb 2021 13:36:17 +0000
• [isabelle] RC5: Sledgehammer and HOL-Library.Word problems
  • Peter Lammich, lammich at in.tum.de - Fri, 12 Feb 2021 12:38:17 +0000
  • Mathias Fleury, mathias.fleury12 at gmail.com - Fri, 12 Feb 2021 12:52:55 +0000
  • Thomas Sewell, tals4 at cam.ac.uk - Mon, 15 Feb 2021 09:57:07 +0000
• [isabelle] RC5: Syntactic class bit_operations is gone
  • Peter Lammich, lammich at in.tum.de - Fri, 12 Feb 2021 13:52:20 +0000
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Fri, 12 Feb 2021 20:17:30 +0000
  • Peter Lammich, lammich at in.tum.de - Fri, 12 Feb 2021 20:42:48 +0000
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Sat, 13 Feb 2021 09:18:49 +0000
  • Peter Lammich, lammich at in.tum.de - Sat, 13 Feb 2021 09:38:04 +0000
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Thu, 25 Feb 2021 16:39:59 +0000
• [isabelle] Relation of function absent from Main
  • Christian Pardillo Laursen, cp735 at cam.ac.uk - Fri, 19 Feb 2021 17:39:03 +0000
  • Tobias Nipkow, nipkow at in.tum.de - Sat, 20 Feb 2021 17:12:14 +0000
  • Dmitriy Traytel, traytel at di.ku.dk - Sat, 20 Feb 2021 21:57:08 +0000
• [isabelle] Remaining uses of "isabelle process" and "isabelle console"
  • Makarius, makarius at sketis.net - Sat, 27 Feb 2021 15:26:50 +0000
• [isabelle] Request for TTP and PTT Interfaces
  • Jens-D. Doll, jens.doll at live.de - Sat, 20 Feb 2021 17:13:18 +0000
  • Makarius, makarius at sketis.net - Tue, 23 Feb 2021 12:58:15 +0000
• [isabelle] Rewrites for a sublocale with UNIV as the carrier set
  • Lukas Stevens, lukas.stevens+isabelle-users at in.tum.de - Fri, 05 Feb 2021 13:15:39 +0000
  • YAMADA, Akihisa, ayamada at trs.cm.is.nagoya-u.ac.jp - Sun, 07 Feb 2021 02:37:41 +0000
  • Lukas Stevens, lukas.stevens+isabelle-users at in.tum.de - Mon, 08 Feb 2021 10:49:48 +0000
  • YAMADA, Akihisa, ayamada at trs.cm.is.nagoya-u.ac.jp - Mon, 08 Feb 2021 12:01:34 +0000
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Mon, 08 Feb 2021 19:38:13 +0000
  • Clemens Ballarin, ballarin at in.tum.de - Sat, 13 Feb 2021 16:52:47 +0000
  • Lukas Stevens, lukas.stevens+isabelle-users at in.tum.de - Tue, 16 Feb 2021 10:35:58 +0000
• [isabelle] SMT 2021 Workshop: Second Call for Papers
  • Nadel, Alexander, alexander.nadel at intel.com - Sun, 28 Feb 2021 06:56:45 +0000
• [isabelle] Some more polishing of the multiset theory
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Sat, 13 Feb 2021 09:51:11 +0000
  • Manuel Eberl, eberlm at in.tum.de - Sat, 13 Feb 2021 10:44:29 +0000
  • Tobias Nipkow, nipkow at in.tum.de - Sun, 14 Feb 2021 17:44:03 +0000
• [isabelle] Syntax proposal: multiway if
  • Manuel Eberl, eberlm at in.tum.de - Wed, 10 Feb 2021 15:07:27 +0000
  • Peter Lammich, lammich at in.tum.de - Wed, 10 Feb 2021 15:41:13 +0000
  • Manuel Eberl, eberlm at in.tum.de - Wed, 10 Feb 2021 15:54:01 +0000
  • Christian Sternagel, c.sternagel at gmail.com - Wed, 10 Feb 2021 18:59:15 +0000
  • Manuel Eberl, eberlm at in.tum.de - Wed, 10 Feb 2021 19:03:08 +0000
  • Gerwin Klein, kleing at unsw.edu.au - Wed, 10 Feb 2021 21:38:22 +0000
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Fri, 19 Feb 2021 15:20:38 +0000
  • Manuel Eberl, eberlm at in.tum.de - Fri, 19 Feb 2021 15:37:17 +0000
• [isabelle] Unfixed variables in "define" command
  • Manuel Eberl, eberlm at in.tum.de - Mon, 22 Feb 2021 12:03:35 +0000
  • Makarius, makarius at sketis.net - Mon, 22 Feb 2021 12:23:15 +0000
  • Jakub Kądziołka, kuba at kadziolka.net - Mon, 22 Feb 2021 12:27:06 +0000
  • Makarius, makarius at sketis.net - Mon, 22 Feb 2021 12:29:08 +0000
  • Manuel Eberl, eberlm at in.tum.de - Mon, 22 Feb 2021 13:29:32 +0000
  • Makarius, makarius at sketis.net - Mon, 22 Feb 2021 14:26:23 +0000
  • Makarius, makarius at sketis.net - Mon, 22 Feb 2021 14:38:53 +0000
• [isabelle] unused_thms in composed theorems
  • Stepan Holub, holub at karlin.mff.cuni.cz - Fri, 19 Feb 2021 14:03:57 +0000
• Re: [isabelle] Weak lemma: HOL-Algebra.Multiplicative_Group.generate_pow_card
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Thu, 25 Feb 2021 16:50:17 +0000
• [isabelle] Weird nesting of Quantifiers
  • Peter Lammich, lammich at in.tum.de - Sun, 14 Feb 2021 15:45:03 +0000
  • Tobias Nipkow, nipkow at in.tum.de - Sun, 14 Feb 2021 17:58:35 +0000
  • Thomas Sewell, tals4 at cam.ac.uk - Mon, 15 Feb 2021 10:16:41 +0000
  • Lawrence Paulson, lp15 at cam.ac.uk - Mon, 15 Feb 2021 10:36:02 +0000
  • Peter Lammich, lammich at in.tum.de - Tue, 16 Feb 2021 12:27:03 +0000
• [isabelle] Yet another Isabelle-Course available
  • Burkhart Wolff, wolff at lri.fr - Wed, 17 Feb 2021 09:02:20 +0000