[Hol-info] WADT 2018 & Leverhulme School - New extension to abstract submission deadline!

[WADT 2018]

==
LAST CALL FOR PAPERS - New extension to abstract submission deadline!

WADT 2018
24th International Workshop on Algebraic Development Techniques
http://wadt18.cs.rhul.ac.uk
July 2–5, 2018, Royal Holloway University of London, Egham, UK

AND

CALL FOR PARTICIPATION - Programme now available!

Leverhulme School on Graph Transformation Techniques 2018
http://wadt18.cs.rhul.ac.uk/lsgt
June 29–July 1, 2018, Royal Holloway University of London, Egham, UK
==

AIMS AND SCOPE

The algebraic approach to system specification encompasses many aspects 
of the formal design of software systems. Originally born as a formal 
method for reasoning about abstract data types, it now covers new 
specification frameworks and programming paradigms (such as 
object-oriented, aspect-oriented, agent-oriented, logic and higher-order 
functional programming) as well as a wide range of application areas 
(including information systems, concurrent, distributed and mobile 
systems). The workshop will provide an opportunity to present recent and 
ongoing work, to meet colleagues, and to discuss new ideas and future 
trends.

TOPICS OF INTEREST

Typical, but not exclusive topics of interest are:
– Foundations of algebraic specification
– Other approaches to formal specification, including process calculi 
and models of concurrent, distributed, and cyber-physical systems
– Specification languages, methods, and environments
– Semantics of conceptual modelling methods and techniques
– Model-driven development
– Graph transformations, term rewriting, and proof systems
– Integration of formal specification techniques
– Formal testing and quality assurance, validation, and verification
– Algebraic approaches to cognitive sciences, including computational 
creativity

WORKSHOP FORMAT AND LOCATION

The workshop will take place over four days, Monday to Thursday, at 
Royal Holloway University of London in Egham, UK 
(https://www.royalholloway.ac.uk).
Presentations will be selected on the basis of submitted abstracts.

Leverhulme School on Graph Transformation Techniques

This occurrence of the ADT workshop will be preceded by the Leverhulme 
School on Graph Transformation Techniques. The school will take place 
over three days, from Friday, June 29th, to Sunday, July 1st, and will 
comprise a self-contained series of invited lectures on graph 
transformation to be given by Reiko Heckel (University of Leicester, 
UK), Fernando Orejas (Technical University of Catalonia, Spain), and 
Detlef Plump (University of York, UK).

INVITED SPEAKERS

Artur d'Avila Garcez (City, University of London, UK)
Rolf Hennicker (LMU Munich, Germany)
Kai-Uwe Kühnberger (Osnabrück University, Germany)
Fernando Orejas (Technical University of Catalonia, Spain)

IMPORTANT DATES

Submission deadline for abstracts: May 18th, 2018
Notification of acceptance: May 25th, 2018
Early registration: June 1st, 2018
Final abstract due: June 8th, 2018
Leverhulme School on Graph Transformation Techniques: June 29–July 1, 2018
ADT Workshop: July 2–5, 2018

SUBMISSIONS

The scientific programme of the workshop will include presentations of 
recent results or ongoing research as well as invited talks. The 
presentations will be selected by the Steering Committee on the basis of 
submitted abstracts according to originality, significance and general 
interest. Abstracts must not exceed two pages including references; if a 
longer version of the contribution is available, it can be made 
accessible on the web and referenced in the abstract.

Abstracts have to be submitted electronically via the EasyChair system 
at https://easychair.org/conferences/?conf=wadt18.

PROCEEDINGS

After the workshop, authors will be invited to submit full papers for 
the refereed proceedings. All submissions will be reviewed by the 
Programme Committee. Selection will be based on originality, soundness, 
and significance of the presented ideas and results. The proceedings 
will be published as a volume of Lecture Notes in Computer Science 
(Springer).

The deadline for submissions will be September 3, 2018, with 
notifications by October 29. Camera-ready versions will be required by 
November 11.

SPONSORSHIP

The workshop takes place under the auspices of IFIP WG 1.3, while the 
series of graph-transformation lectures is supported by a Leverhulme 
Trust Visiting Professorship.

WADT STEERING COMMITTEE

Andrea Corradini (Italy)
José Fiadeiro (UK) [co-chair]
Rolf Hennicker (Germany)
Hans-Jörg Kreowski (Germany)
Till Mossakowski (Germany)
Fernando Orejas (Spain)
Markus Roggenbach (UK)
Grigore Roșu (United States)

PROGRAMME COMMITEE

Paolo Baldan (Italy)
Andrea Corradini (Italy)
Artur d'Avila Garcez (UK)
Răzvan Diaconescu (Romania)
José Fiadeiro (UK) [co-chair]
Fabio Gadducci (Italy)
Reiko Heckel (UK)
Rolf Hennicker (Germany)
Alexander Knapp (Germany)
Barbara König (Germany)

Re: [Hol-info] Extension of Co-algebraic Datatype

[Michael.Norrish]

If you want the coinductively defined streams predicate over lllist, you can 
write

>  CoIndDefLib.Hol_coreln `!a s. a IN A /\ streams A s ==> streams A (LCONS a 
> s)`;

<>

<>

val it =

   (⊢ ∀A a s. a ∈ A ∧ streams A s ⇒ streams A (a:::s),

⊢ ∀A streams'.

  (∀a0. streams' a0 ⇒ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams' s) ⇒

  ∀a0. streams' a0 ⇒ streams A a0,

⊢ ∀A a0. streams A a0 ⇔ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams A s):

I think the last theorem of the triple is the cases theorem you want.

Note that if you are going to define Stream with

  Stream L = LFILTER (\n. T) L

You might as well write the equivalent

  Stream L = L

Best wishes,
Michael



From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Saturday, 12 May 2018 at 05:45
To: "Norrish, Michael (Data61, Acton)" 
Cc: hol-info 
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Thanks!. I understand that the working of LNIL and LCONS constructors since I'm 
exploring "llistTheory" for quite some time. To be very clear, I'm in the 
process of porting "stream theory" form Isabelle 
https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html which 
is formalized as coinductive "stream":

codatatype (sset: 'a) stream =
  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
for
  map: smap
  rel: stream_all2

 I can see that its datatype is very similar to lazy list (llistTheory) 
datatype so rather defining a new type I defined a function that returns the 
same 'a llist-typed (lazy) list as given to its input:

∀​​L. Stream L = LFILTER (λ​​n. T) L:

type_of ``stream``;

 ``:α​​ llist -> α​​ llist``:


Later in Isabelle "stream theory", a coinductive set "streams" is defined based 
on "stream" datatype as:

coinductive_set
  streams :: "'a set ⇒​​  'a stream set"
  for A :: "'a set"
where
  Stream[intro!, simp, no_atp]: "[[a ∈​​ A; s ∈​​ streams A]] ⟹ a ## s ∈​​ 
streams A"
end

Using llistTheory functions, I'm able to define a similar function as:

∀​​A. streams A = IMAGE (λ​​a. Stream a) {llist_abs (λ​​n. SOME x) | x ∈​​ A}:

type_of ``streams``;

 ``:('a -> bool) -> 'a llist -> bool``:

However, by using shallow embedding approach, I'm not able to use some 
essential properties that are accompanied when a new coinductive datatype is 
defined. For instance, if a streams datatype is define, I may have this 
property of form:

streams.cases (Isabelle):

a ∈​​ streams A ⇒​​ (? a s. a = a ##s ⇒​​ a ∈​​ A ⇒​​ s ∈​​  streams A ⇒​​ P) 
⇒​​ P

I'm having the issues of defining these types in HOL4. Is there any way that I 
can replicate the same in HOL4?


On Mon, May 7, 2018 at 8:49 PM, 
> wrote:
You can probably define a function of that type, but you can’t define a 
*constructor* of that type for llist.   (Contrast what I’d consider to be 
llist’s standard constructors, LNIL and LCONS. They have types α llist, and α 
-> α llist -> α llist respectively.)

You said you wanted a stream type, does this mean you want a constructor for 
stream of type

  (α -> bool) -> α stream

?

Such a constructor is not recursive, so I can just write

Datatype`stream = SetConstructor (α -> bool)`

The SetConstructor term then has the desired type.

So I’m afraid I still don’t understand your question.

Michael

From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Monday, 7 May 2018 at 11:38
To: "Norrish, Michael (Data61, Acton)" 
>
Cc: hol-info 
>
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Thanks for the explanation. Let me state it clearly. Can I write down a 
constructor of type

(α -> bool) -> α​​ llist



On Sun, May 6, 2018 at 8:39 PM, 
> wrote:
I think you may be able to make your needs more precise by explicitly 
considering what your co-algebra would be.

In particular, write down the type of the “general” destructor

  myType -> F(myType)

For lazy lists, this is

  α llist -> (α # α llist) option

For the co-algebraic numbers it’s

  num -> num option

For arbitrarily (but finite)-branching trees, it’s

  Tree -> Tree list

(If you change list to llist you get possibly infinitely branching trees.)

In the lazy lists, this destructor might be called “HDTL”; in the numbers, it’s 
“predecessor”; in the trees it’s “children”.  Because the types are 
co-algebraic each might be iterable an infinite number of times.  (The 
corresponding destructors in the algebraic types are always well-founded.)

What are the co-algebras for your desired types?  I don’t think I’ve understood 
what you want, but it superficially appears as if you want dependent types, 
where you combine the type with some term-level predicate. That sort of