Cl-isabelle-users April 2021 Archives by author

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

• Achim D. Brucker, brucker at spamfence.net
  • [isabelle] Announcement: Isabelle/DOF 1.1.0 - Tue, 06 Apr 2021 19:46:30 +0100
• Alexander Baumgartner via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
  • [isabelle] UNIF 2021: second call for papers - Thu, 01 Apr 2021 05:36:10 +0100
• Alex Meyer, alex153 at outlook.lv
  • [isabelle] Pārs.: Parsing term is easy with Scala, can similar approach be applied to the theory? - Sun, 04 Apr 2021 23:49:20 +0100
  • [isabelle] Atb.: Is it possible to use QRHL tool without reference to QRHL theories? - Wed, 28 Apr 2021 18:07:43 +0100
  • [isabelle] Pārs.: Parsing term is easy with Scala, can similar approach be applied to the theory? - Sun, 04 Apr 2021 14:16:11 +0100
  • [isabelle] Parsing term is easy with Scala, can similar approach be applied to the theory? - Sun, 04 Apr 2021 13:37:01 +0100
  • [isabelle] How to get TopLevel.state from the theorem string (initiate proof and make one proof step) and is it possible to do this from QRHL tool? - Wed, 28 Apr 2021 23:43:12 +0100
  • [isabelle] Can QRHL tool be used without QRHL theories, for just some simple (non-quantum) theories? - Wed, 28 Apr 2021 17:34:51 +0100
• Andreas Lochbihler, mail at andreas-lochbihler.de
  • [isabelle] Two new AFP entries: Gale-Stewart games and Isabelle's Metalogic: Formalization and Proof Checker - Wed, 28 Apr 2021 09:36:26 +0100
  • [isabelle] New AFP entry: Information Flow Control via Dependency Tracking - Thu, 01 Apr 2021 11:14:30 +0100
• Bo Gan, gan.bo at columbia.edu
  • [isabelle] High CPU usage on PolyML subprocess (Pure/HOL), Isabelle GUI (JEdit) getting sluggish - Tue, 27 Apr 2021 03:29:11 +0100
• Chantal Keller, chantal.keller at wanadoo.fr
  • [isabelle] 7th International Workshop on Proof eXchange for Theorem Proving (PxTP) - Second CFP - Mon, 12 Apr 2021 16:56:00 +0100
  • [isabelle] 7th International Workshop on Proof eXchange for Theorem Proving (PxTP) - DEADLINE EXTENSION: May 5 - Thu, 22 Apr 2021 16:11:27 +0100
• Clemens Ballarin, ballarin at in.tum.de
  • Re: [isabelle] Issues with locale interpretation - Sun, 11 Apr 2021 10:52:47 +0100
• Dmitriy Traytel, traytel at di.ku.dk
  • Re: [isabelle] Datatype definition can be slow - Wed, 14 Apr 2021 00:02:16 +0100
  • Re: [isabelle] Datatype definition can be slow - Tue, 13 Apr 2021 15:50:46 +0100
• Dominique Unruh, unruh at ut.ee
  • Re: [isabelle] Parsing term is easy with Scala, can similar approach be applied to the theory? - Mon, 05 Apr 2021 01:08:50 +0100
  • Re: [isabelle] parse_translation does not detect changes in theory data - Fri, 30 Apr 2021 11:21:53 +0100
  • Re: [isabelle] Printing a term without abbreviations/notation - Tue, 20 Apr 2021 11:59:07 +0100
  • Re: [isabelle] Datatype definition can be slow - Tue, 13 Apr 2021 17:07:04 +0100
  • Re: [isabelle] Datatype definition can be slow - Tue, 13 Apr 2021 17:36:51 +0100
• Dr A. Koutsoukou-Argyraki, ak2110 at cam.ac.uk
  • Re: [isabelle] Announcing SErAPIS: a new search engine for Isabelle - Mon, 19 Apr 2021 14:28:02 +0100
  • [isabelle] Announcing SErAPIS: a new search engine for Isabelle - Mon, 19 Apr 2021 12:14:01 +0100
• Enrico Tassi, Enrico.Tassi at inria.fr
  • [isabelle] [CFP] Logical Frameworks and Meta-Languages: Theory and Practice - Extended Deadline - Mon, 19 Apr 2021 14:10:33 +0100
  • [isabelle] [CFP] Logical Frameworks and Meta-Languages: Theory and Practice - Sun, 11 Apr 2021 13:59:44 +0100
  • [isabelle] [CFP] Logical Frameworks and Meta-Languages: Theory and Practice - Fri, 16 Apr 2021 13:32:07 +0100
• Eugene W. Stark, isabelle-users at starkeffect.com
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Fri, 23 Apr 2021 02:51:22 +0100
  • [isabelle] Quickcheck reports an incorrect counterexample - Sun, 11 Apr 2021 14:56:05 +0100
• Fabian Huch, huch at in.tum.de
  • Re: [isabelle] Failed call to isabelle jedit -R with code generation in thy's - Tue, 27 Apr 2021 11:56:46 +0100
• Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
  • Re: [isabelle] Quickcheck reports an incorrect counterexample - Fri, 16 Apr 2021 06:27:40 +0100
• Gerwin Klein, kleing at unsw.edu.au
  • Re: [isabelle] Lemma like shiftr_bl but for sshiftr in Word Library - Sun, 18 Apr 2021 23:21:44 +0100
• He, Shuhan, 13061136 at buaa.edu.cn
  • [isabelle] Datatype definition can be slow - Mon, 12 Apr 2021 15:39:59 +0100
  • Re: [isabelle] Datatype definition can be slow - Fri, 16 Apr 2021 03:39:30 +0100
• Jason Gross, jasongross9 at gmail.com
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Thu, 22 Apr 2021 13:56:49 +0100
• Laarman, A.W., a.w.laarman at liacs.leidenuniv.nl
  • [isabelle] SPIN 2021 - Final Call for Papers - Mon, 19 Apr 2021 11:20:26 +0100
• Lawrence Paulson, lp15 at cam.ac.uk
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Wed, 21 Apr 2021 11:58:42 +0100
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Wed, 21 Apr 2021 12:17:39 +0100
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Fri, 23 Apr 2021 12:29:05 +0100
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Thu, 22 Apr 2021 10:37:50 +0100
  • [isabelle] Issues with locale interpretation - Fri, 09 Apr 2021 12:23:34 +0100
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Fri, 23 Apr 2021 12:37:12 +0100
  • Re: [isabelle] Issues with locale interpretation - Sun, 11 Apr 2021 18:01:24 +0100
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Thu, 22 Apr 2021 10:45:48 +0100
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Fri, 23 Apr 2021 12:03:35 +0100
  • [isabelle] new in the AFP: The BKR Decision Procedure for Univariate Real Arithmetic - Sun, 25 Apr 2021 16:40:00 +0100
• Lukas Stevens, lukas.stevens+isabelle-users at in.tum.de
  • Re: [isabelle] Editing the Isabelle Wiki - Thu, 08 Apr 2021 11:40:13 +0100
• MACKENZIE Carlin, s1724780 at sms.ed.ac.uk
  • [isabelle] Results — Survey on the AFP - Tue, 06 Apr 2021 10:11:35 +0100
• Makarius, makarius at sketis.net
  • Re: [isabelle] Failed call to isabelle jedit -R with code generation in thy's - Tue, 27 Apr 2021 23:42:19 +0100
  • Re: [isabelle] Failed call to isabelle jedit -R with code generation in thy's - Tue, 27 Apr 2021 23:45:26 +0100
  • Re: [isabelle] Symbolic execution in Isabelle. - Mon, 19 Apr 2021 12:21:49 +0100
  • Re: [isabelle] export code checking OCaml: zarith not found - Tue, 06 Apr 2021 13:07:44 +0100
  • Re: [isabelle] Editing the Isabelle Wiki - Thu, 08 Apr 2021 10:59:14 +0100
  • Re: [isabelle] Symbolic execution in Isabelle. - Mon, 19 Apr 2021 11:14:20 +0100
• Manuel Eberl, eberlm at in.tum.de
  • Re: [isabelle] Possible problem with floating-point addition in Approximation etc. - Wed, 07 Apr 2021 16:34:53 +0100
  • [isabelle] Printing a term without abbreviations/notation - Tue, 20 Apr 2021 10:30:56 +0100
  • Re: [isabelle] Term to be evaluated contains free dictionaries - Wed, 28 Apr 2021 12:08:19 +0100
  • Re: [isabelle] Printing a term without abbreviations/notation - Tue, 20 Apr 2021 12:03:38 +0100
  • Re: [isabelle] Datatype definition can be slow - Tue, 13 Apr 2021 17:11:49 +0100
  • Re: [isabelle] Datatype definition can be slow - Tue, 13 Apr 2021 16:01:12 +0100
  • Re: [isabelle] Datatype definition can be slow - Tue, 13 Apr 2021 17:16:06 +0100
• Marco David, mdavid8101 at gmail.com
  • [isabelle] Editing the Isabelle Wiki - Wed, 07 Apr 2021 17:12:21 +0100
• Marmsoler, Diego, D.Marmsoler at exeter.ac.uk
  • [isabelle] FMBC: Second Call for Papers - Fri, 09 Apr 2021 09:53:19 +0100
  • [isabelle] FMBC 2021 - 3rd Call for Papers (Deadline extensions) - Sat, 24 Apr 2021 17:30:23 +0100
• Matthys Grobbelaar, m.grobbelaar at uq.net.au
  • [isabelle] parse_translation does not detect changes in theory data - Fri, 30 Apr 2021 02:34:37 +0100
  • [isabelle] Using the global context when performing syntax translations - Sun, 25 Apr 2021 07:18:21 +0100
• Mikhail Chekhov, mikhail.chekhov.w at gmail.com
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Sat, 24 Apr 2021 23:41:25 +0100
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Sat, 24 Apr 2021 01:33:56 +0100
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Sat, 24 Apr 2021 01:19:04 +0100
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Thu, 22 Apr 2021 22:06:36 +0100
  • [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Tue, 20 Apr 2021 20:01:25 +0100
  • Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion - Wed, 21 Apr 2021 19:37:39 +0100
• Mikhail Mandrykin, mandrykin at ispras.ru
  • [isabelle] Exhaustiveness of Pure.type - Fri, 16 Apr 2021 20:05:53 +0100
• Moscato, Mariano M. (LARC-D320)[NATIONAL INSTITUTE OF AEROSPACE] via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
  • [isabelle] NASA Formal Methods 2021: Call for (virtual) participation - Tue, 27 Apr 2021 12:14:01 +0100
• Nadel, Alexander, alexander.nadel at intel.com
  • [isabelle] SMT 2021 Workshop: Deadline Extension to May 7 - Fri, 30 Apr 2021 21:29:46 +0100
  • [isabelle] SMT 2021 Workshop: Final Call for Papers - Wed, 14 Apr 2021 06:33:18 +0100
• Peter Gammie, peteg42 at gmail.com
  • Re: [isabelle] Symbolic execution in Isabelle. - Mon, 19 Apr 2021 02:03:46 +0100
• Peter Lammich, lammich at in.tum.de
  • Re: [isabelle] Recurring error from Isabelle Syslog - Fri, 30 Apr 2021 15:58:38 +0100
  • [isabelle] export code checking OCaml: zarith not found - Tue, 06 Apr 2021 12:48:49 +0100
  • Re: [isabelle] export code checking OCaml: zarith not found - Tue, 06 Apr 2021 15:09:15 +0100
  • [isabelle] isabelle ghc_setup - Tue, 13 Apr 2021 17:15:03 +0100
  • Re: [isabelle] Printing a term without abbreviations/notation - Tue, 20 Apr 2021 12:11:08 +0100
• Sandra Alves, sandra at dcc.fc.up.pt
  • [isabelle] Women in Logic 2021 - Call for Participation - Mon, 19 Apr 2021 14:04:57 +0100
• Serge Autexier, serge.autexier at dfki.de
  • [isabelle] 2021 Conference on Intelligent Computer Mathematics - Doctoral Programme - Call for Abstracts - Mon, 19 Apr 2021 08:20:59 +0100
• Stepan Holub, holub at karlin.mff.cuni.cz
  • Re: [isabelle] Term to be evaluated contains free dictionaries - Wed, 28 Apr 2021 11:06:00 +0100
  • [isabelle] Term to be evaluated contains free dictionaries - Wed, 28 Apr 2021 10:41:10 +0100
• Thomas Melham, tom.melham at cs.ox.ac.uk
  • [isabelle] Symbolic execution in Isabelle. - Sat, 17 Apr 2021 12:35:04 +0100
• Thomas Sewell, tals4 at cam.ac.uk
  • Re: [isabelle] Symbolic execution in Isabelle. - Mon, 19 Apr 2021 21:23:40 +0100
• Tjark Weber, tjark.weber at it.uu.se
  • [isabelle] CfP: Logical Frameworks and Meta-Languages: Theory and Practice - Mon, 19 Apr 2021 15:32:17 +0100
• Tobias Nipkow, nipkow at in.tum.de
  • [isabelle] New in the AFP: Formalization of Timely Dataflow's Progress Tracking Protocol - Fri, 16 Apr 2021 06:46:54 +0100
  • Re: [isabelle] Quickcheck reports an incorrect counterexample - Mon, 12 Apr 2021 10:15:27 +0100
• Thiemann, René, Rene.Thiemann at uibk.ac.at
  • [isabelle] New in the AFP: Grothendieck's Schemes in Algebraic Geometry - Fri, 09 Apr 2021 14:38:50 +0100
• Florian Märkl, isabelle-users at florianmaerkl.de
  • [isabelle] Lemma like shiftr_bl but for sshiftr in Word Library - Sun, 18 Apr 2021 19:35:26 +0100
  • Re: [isabelle] Failed call to isabelle jedit -R with code generation in thy's - Wed, 28 Apr 2021 09:02:38 +0100
  • [isabelle] Generic Lemma about Sums of Powers divided by their Base (also for right bit shifts) - Wed, 28 Apr 2021 15:24:22 +0100
• Jakub Kądziołka, kuba at kadziolka.net
  • Re: [isabelle] Recurring error from Isabelle Syslog - Fri, 30 Apr 2021 15:57:24 +0100
  • Re: [isabelle] Datatype definition can be slow - Tue, 13 Apr 2021 17:14:32 +0100
  • Re: [isabelle] Term to be evaluated contains free dictionaries - Wed, 28 Apr 2021 10:48:17 +0100
• Jonathan Julián Huerta y Munive, jonjulian23 at gmail.com
  • [isabelle] Failed call to isabelle jedit -R with code generation in thy's - Tue, 27 Apr 2021 10:26:29 +0100
• Yakoub Nemouchi, y.nemouchi at gmail.com
  • [isabelle] Recurring error from Isabelle Syslog - Fri, 30 Apr 2021 15:51:50 +0100
• Yiannos A. Stathopoulos, yas23 at cam.ac.uk
  • Re: [isabelle] Announcing SErAPIS: a new search engine for Isabelle - Mon, 19 Apr 2021 17:04:16 +0100