[Hol-info] PPDP 2018: First Call for Papers

==     PPDP 2018: First Call for Papers == 20th International Symposium on     Principles and Practice of Declarative Programming

[Hol-info] Introduction of new types in PVS, HOL, and R0 – Re: Inquiry: Introducing new types as predicates

Dear Cris, Links to two different PVS papers on this topic are provided at: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-October/msg00050.html http://lists.seas.upenn.edu/pipermail/types-list/2017/001971.html The disadvantage of the PVS subtype implementation in my o

Re: [Hol-info] Inquiry: Introducing new types as predicates

On 23/01/18 12:16, Mario Castelán Castro wrote: > For example, in HOL4 you have the seemingly > universal type {x | T} Correction: I meant “the seemingly universal set”. signature.asc Description: OpenPGP digital signature

Re: [Hol-info] Inquiry: Introducing new types as predicates

On 22/01/18 18:35, Cris Perdue wrote: > Are any of you readers of this list aware of investigations or > implementations of logics that, like the HOL family of provers, are based > on the simple theory of types, but which support introduction of new types > through new predicates rather than new ty

[Hol-info] ABZ 2018, extended deadline: 5th February

ABZ 2018 6th International ABZ (ASM, Alloy, B, TLA, VDM, Z) Conference June 5th-8th, 2018 Southampton, UK www.southampton.ac.uk/abz2018 The ABZ conference is dedicated to the cross-fertilization of six related state-based and machine-based formal methods, Abs