Termination-Portal.org - User contributions [en]

Tools:Rainbow

2011-01-18T09:13:00Z

Blanqui:

{{Tool
|shortname=Rainbow
|longname=Termination proof certifier
|homepage=http://color.inria.fr/
|country=France and The Netherlands
|university=INRIA and Eindhoven University of Technology
|developers=Frederic Blanqui and Adam Koprowski
|publication=[[Bibtex:CoLoR11|Bibtex:CoLoR11]]
}}

Tools:CoLoR

2011-01-18T09:12:33Z

Blanqui:

{{Tool
|shortname=CoLoR
|longname=Coq Library on Rewriting and termination
|homepage=http://color.inria.fr/
|country=France and The Netherlands
|university=INRIA and Eindhoven University of Technology
|developers=[[People:Frederic Blanqui|Frederic Blanqui]] and [[People:Adam Koprowski|Adam Koprowski]]
|publication=[[Bibtex:CoLoR11|Bibtex:CoLoR11]]
}}

Bibtex:CoLoR11

2011-01-18T09:12:01Z

Blanqui:

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>
@ARTICLE{blanqui11mscs,
AUTHOR = {F. Blanqui and A. Koprowski},
TITLE = {CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates},
JOURNAL = {Mathematical Structures in Computer Science},
YEAR = {2011},
VOLUME = {?},
NUMBER = {?},
PAGES = {?-?},
NOTE = {To appear}}
</bibtex>

Bibtex:CoLoR11

2011-01-18T09:11:39Z

Blanqui: Created page with "  == BibTex == ..."

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>
@ARTICLE{blanqui11mscs,
AUTHOR = {F. Blanqui and A. Koprowski},
TITLE = {{CoLoR}: a {Coq} library on well-founded rewrite relations and its application to the automated verification of termination certificates},
JOURNAL = {Mathematical Structures in Computer Science},
YEAR = {2011},
VOLUME = {?},
NUMBER = {?},
PAGES = {?-?},
NOTE = {To appear}}
</bibtex>

Tools:Rainbow

2009-10-29T02:06:49Z

Blanqui:

{{Tool
|shortname=Rainbow
|longname=Termination proof certifier
|homepage=http://color.inria.fr/
|country=France and The Netherlands
|university=INRIA and Eindhoven University of Technology
|developers=Frederic Blanqui and Adam Koprowski
|publication=[[Bibtex:CoLoR09|Bibtex:CoLoR09]]
}}

Bibtex:CoLoR09

2009-06-03T07:13:09Z

Blanqui:

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>
@TechReport{CoLoR09,
author = {F. Blanqui and A. Koprowski},
title = {Automated verification of termination certificates},
institution = {INRIA Rocquencourt, France},
year = 2009,
number = 6949,
url = {http://www-rocq.inria.fr/~blanqui/rr6949-pdf.html}}
</bibtex>

Bibtex:CoLoR06

2009-06-03T07:12:42Z

Blanqui:

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>
@INPROCEEDINGS{blanqui06wst-color,
AUTHOR = {F. Blanqui and S. Coupet-Grimal and W. Delobel and S. Hinderer and A. Koprowski},
TITLE = {CoLoR: a Coq Library on Rewriting and termination},
BOOKTITLE = {Proceedings of the 8th International Workshop on Termination (WST)},
YEAR = 2006,
url = {http://www-rocq.inria.fr/~blanqui/wst06color-pdf.html}}
</bibtex>

Bibtex:CoLoR09

2009-06-03T07:10:53Z

Blanqui:

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>
@TechReport{CoLoR09,
author = {F. Blanqui and A. Koprowski},
title = {Automated verification of termination certificates},
institution = {INRIA Rocquencourt, France},
year = 2009,
number = 6949,
url = {http://www-rocq.inria.fr/~blanqui/papers/rr6949-pdf.html}}
</bibtex>

Bibtex:CoLoR09

2009-06-03T06:50:00Z

Blanqui:

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>
@TechReport{CoLoR09,
author = {F. Blanqui and A. Koprowski},
title = {Automated verification of termination certificates},
institution = {INRIA Rocquencourt, France},
year = 2009,
number = 6949,
url = {http://color.inria.fr/}}
</bibtex>

Tools:CoLoR

2009-06-03T06:49:18Z

Blanqui:

{{Tool
|shortname=CoLoR
|longname=Coq Library on Rewriting and termination
|homepage=http://color.inria.fr/
|country=France and The Netherlands
|university=INRIA and Eindhoven University of Technology
|developers=[[People:Frederic Blanqui|Frederic Blanqui]] and [[People:Adam Koprowski|Adam Koprowski]]
|publication=[[Bibtex:CoLoR09|Bibtex:CoLoR09]]
}}

Bibtex:CoLoR09

2009-06-03T06:47:33Z

Blanqui:

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>
@TechReport{CoLoR09,
author = {F. Blanqui and A. Koprowski},
title = {Automated verification of termination certificates},
institution = {INRIA Rocquencourt, France},
year = 2009,
number = 6949}
</bibtex>

Bibtex:CoLoR09

2009-06-03T06:47:08Z

Blanqui:

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>
@TechReport{CoLoR09,
author = {F. Blanqui and A. Koprowski},
title = {Automated verification of termination certificates},
institution = {INRIA Rocquencourt, France},
year = 2009,
type = {Research Report},
number = 6949}
</bibtex>

Bibtex:CoLoR09

2009-06-03T06:46:22Z

Blanqui: New page:  == BibTex ==  <bibtex> ...

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>
@TechReport{CoLoR09,
author = {F. Blanqui and A. Koprowski},
title = {Automated verification of termination certificates},
institution = {INRIA Rocquencourt, France},
year = 2009,
number = 6949}
</bibtex>

Tools:CoLoR

2009-05-14T02:03:19Z

Blanqui:

{{Tool
|shortname=CoLoR
|longname=Coq Library on Rewriting and termination
|homepage=http://color.inria.fr/
|country=France and The Netherlands
|university=INRIA and Eindhoven University of Technology
|developers=[[People:Frederic Blanqui|Frederic Blanqui]] and [[People:Adam Koprowski|Adam Koprowski]]
|publication=[[Bibtex:CoLoR06|Bibtex:CoLoR06]]
}}

Tools:CoLoR

2009-05-14T02:03:01Z

Blanqui:

{{Tool
|shortname=CoLoR
|longname=Coq Library on Rewriting and termination
|homepage=http://color.inria.fr/
|country=France and The Netherlands
|university=INRIA and Eindhoven University of Technology
|developers=[[People:Frederic Blanqui|Frederic Blanqui]] and [[People:Adam Koprowski|Adam Koprowski]]
|publication=
}}

Bibtex:CoLoR06

2009-05-14T02:02:07Z

Blanqui:

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>
@INPROCEEDINGS{blanqui06wst-color,
AUTHOR = {F. Blanqui and S. Coupet-Grimal and W. Delobel and S. Hinderer and A. Koprowski},
TITLE = {CoLoR: a Coq Library on Rewriting and termination},
BOOKTITLE = {Proceedings of the 8th International Workshop on Termination (WST)},
YEAR = 2006,
NOTE = {\url{http://color.inria.fr/}}}
</bibtex>

Bibtex:CoLoR06

2009-05-14T02:01:41Z

Blanqui: New page:  == BibTex ==  <bibtex> ...

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>
@INPROCEEDINGS{blanqui06wst-color,
AUTHOR = {F. Blanqui and S. Coupet-Grimal and W. Delobel and S. Hinderer and A. Koprowski},
TITLE = {{CoLoR}: a {C}oq {L}ibrary on {R}ewriting and termination},
BOOKTITLE = {Proceedings of the 8th International Workshop on Termination (WST)},
YEAR = 2006,
NOTE = {\url{http://color.inria.fr/}}}
</bibtex>

People:Frederic Blanqui

2009-05-14T01:54:53Z

Blanqui:

{{Person
|firstname=Frederic
|middlenames=
|lastname=Blanqui
|titles=
|email=
|homepage=http://www-rocq.inria.fr/~blanqui/
|country=France
|university=INRIA
|department=
|role=Researcher
}}

Tools:CoLoR

2009-05-14T01:54:10Z

Blanqui:

{{Tool
|shortname=CoLoR
|longname=Coq Library on Rewriting and termination
|homepage=http://color.inria.fr/
|country=France and The Netherlands
|university=INRIA and Eindhoven University of Technology
|developers=[[People:Frederic Blanqui|Frederic Blanqui]] and [[People:Adam Koprowski|Adam Koprowski]]
|publication=
}}

People:Frederic Blanqui

2009-04-10T05:50:36Z

Blanqui:

{{Person
|firstname=Frederic
|middlenames=
|lastname=Blanqui
|titles=
|email=
|homepage=http://www-rocq.inria.fr/~blanqui/
|country=France
|university=INRIA
|department=
|role=Researcher 
}}

Termination Competition Platform

2008-11-21T05:58:22Z

Blanqui: /* Wishlist: Query Interface */

= Note =

There is (will be) a well-defined process of making design decisions w.r.t. the Termination Competition Execution and Presentation Platform (via mailing list, steering committee), and then the Host decides on implementation.

For features that have run through this process, the [http://dev.aspsimon.org/bugzilla/buglist.cgi?bug_file_loc=&bug_file_loc_type=allwordssubstr&bug_id=&bug_status=NEW&bug_status=ASSIGNED&bug_status=REOPENED termcomp Bugzilla] is the right place for bug reports.

Below here, we just collect some ideas for later consideration.

= Wishlist: Query Interface =

The idea is to provide a web interface for queries over the results data base(s).
We aim for flexibility, but will start with some simple prototype.
Please list here some typical queries that you would want to execute.

* what problems were solved in srs-standard, but not in srs-standard-certified?
* what are the problems that were solved in (insert category here)-2008 but not in 2007 (yes, we plan to import earlier competition results into the data base)?
* what is the problem/tool in (insert category here) with the longest/shortest proof (file size)/execution time?

* what are the problems that generate a coq timeout for some tool?
* what is the average size of the (xml|coq) files generated by a given tool?
* what are the (problems|results) that are (solved|certified) by all the tools in some set of tools?

what might also be helpful: can you name a web site with some configurable query functionality
that you think is especially well-designed and worth learning from?

Christian Sternagel: I would also like to be able to query the problem data base and not only the results data base(s). (J.W.: there is a [http://colo5-c703.uibk.ac.at:8080/termcomp/tpdb/tpsearch.seam query interface for tpdb] already. what features are missing? C.S.: Since it is currently not working, it is merely a placeholder for a query interface.)

Missing features:

* give me all problems from 2007 that are left linear/overlapping/dummy SRSs/... (i.e., properties of problems)
* boolean combination of properties
* wild cards

WScT08

2008-04-21T09:54:08Z

Blanqui: /* Options for location */

= Workshop on Certified Termination WScT08 =

For general information on the workshop topic and history, see [[WScT]].

This will be a working meeting,
with plenty of room for discussion.

* location: Leipzig, Germany
* date: May 17 - 19, 2008
* local organizer: Johannes Waldmann, HTWK Leipzig

== Registration/Program ==

Please register by writing your name here
and the title of the talk you want to give,
or the topic you want to discuss.
(Feel free to create wiki pages for your topic, and link from here.)

* Johannes Waldmann, topics I'd like to see
** the present of Rainbow (give help to people who want to use this, may include some time for actual implementation/hacking)
** future of Rainbow (what has become of the plans we made http://color.loria.fr/workshop.html)

* Christian Sternagel, (Topic: TBA)

* Adam Koprowski, (topic: TBA)

* René Thiemann, topics to present (in combination with other colleagues from Innsbruck) and discuss
** presentation of (fixed) details on upcoming termination competition (TC)
** discussion of TC-details that have to be fixed by the community

* Frederic Blanqui. I can present the current state of Rainbow and CoLoR.

* Carsten Fuhs, (topic: TBA)

== Local Organization ==

Details will be fixed soon. Vote here! (Just mark with "X")

=== Options for location ===

* external conference facility (e.g. http://www.mediencampus-villa-ida.de/ ,rent would be 150 EUR per day), on-site restaurant/catering (additional cost)

* (XXXX) classroom at HTWK (e.g. "Lipsius-Bau" on that map: http://www.htwk-leipzig.de/hochsch/lageplan.pdf , low or no cost) , self-catering (several small restaurants nearby)

=== Options for date/time ===

* workshop start: Saturday
** (XXX) morning (9 a.m.) or
** (X) noon (1 p.m.)
* Workshop Dinner (Sunday), booking a table at some restaurant
** in the city center
** (XX) outskirts (may include walk or tram ride)
* workshop end: Monday
** (XXX) noon (1 p.m.) or
** afternoon (5 p.m.)

== Accomodation ==

You'll find plenty of hotels of all price ranges through the usual
[http://maps.google.de/maps?f=l&hl=de&geocode=&q=hotel&near=Leipzig+Gustav+Freytag+Stra%C3%9Fe&sll=51.315754,12.37009&sspn=0.039108,0.076733&ie=UTF8&ll=51.313823,12.37421&spn=0.019555,0.038366&z=15 search engines]

HTWK is at Karl-Liebknecht-Straße/Richard-Lehmann-Straße.

(note: Hotel Seeblick is not a hotel. And there is no Lake.)

== Adjacent event(s) ==

Note that WScT08 is right after
[http://www.orchid.inf.tu-dresden.de/gdp/wata08/ WATA08 Dresden].
(There will even be some termination talks at WATA.)
Travel from Dresden to Leipzig is easy (one hour by train).
Dresden is a major tourist attraction.

WScT08

2008-04-21T09:53:46Z

Blanqui: /* Options for date/time */

= Workshop on Certified Termination WScT08 =

For general information on the workshop topic and history, see [[WScT]].

This will be a working meeting,
with plenty of room for discussion.

* location: Leipzig, Germany
* date: May 17 - 19, 2008
* local organizer: Johannes Waldmann, HTWK Leipzig

== Registration/Program ==

Please register by writing your name here
and the title of the talk you want to give,
or the topic you want to discuss.
(Feel free to create wiki pages for your topic, and link from here.)

* Johannes Waldmann, topics I'd like to see
** the present of Rainbow (give help to people who want to use this, may include some time for actual implementation/hacking)
** future of Rainbow (what has become of the plans we made http://color.loria.fr/workshop.html)

* Christian Sternagel, (Topic: TBA)

* Adam Koprowski, (topic: TBA)

* René Thiemann, topics to present (in combination with other colleagues from Innsbruck) and discuss
** presentation of (fixed) details on upcoming termination competition (TC)
** discussion of TC-details that have to be fixed by the community

* Frederic Blanqui. I can present the current state of Rainbow and CoLoR.

* Carsten Fuhs, (topic: TBA)

== Local Organization ==

Details will be fixed soon. Vote here! (Just mark with "X")

=== Options for location ===

* external conference facility (e.g. http://www.mediencampus-villa-ida.de/ ,rent would be 150 EUR per day), on-site restaurant/catering (additional cost)

* (XXX) classroom at HTWK (e.g. "Lipsius-Bau" on that map: http://www.htwk-leipzig.de/hochsch/lageplan.pdf , low or no cost) , self-catering (several small restaurants nearby)

=== Options for date/time ===

* workshop start: Saturday
** (XXX) morning (9 a.m.) or
** (X) noon (1 p.m.)
* Workshop Dinner (Sunday), booking a table at some restaurant
** in the city center
** (XX) outskirts (may include walk or tram ride)
* workshop end: Monday
** (XXX) noon (1 p.m.) or
** afternoon (5 p.m.)

== Accomodation ==

You'll find plenty of hotels of all price ranges through the usual
[http://maps.google.de/maps?f=l&hl=de&geocode=&q=hotel&near=Leipzig+Gustav+Freytag+Stra%C3%9Fe&sll=51.315754,12.37009&sspn=0.039108,0.076733&ie=UTF8&ll=51.313823,12.37421&spn=0.019555,0.038366&z=15 search engines]

HTWK is at Karl-Liebknecht-Straße/Richard-Lehmann-Straße.

(note: Hotel Seeblick is not a hotel. And there is no Lake.)

== Adjacent event(s) ==

Note that WScT08 is right after
[http://www.orchid.inf.tu-dresden.de/gdp/wata08/ WATA08 Dresden].
(There will even be some termination talks at WATA.)
Travel from Dresden to Leipzig is easy (one hour by train).
Dresden is a major tourist attraction.

WScT08

2008-04-15T09:20:00Z

Blanqui: /* Registration/Program */

= Workshop on Certified Termination WScT08 =

This will be a working meeting,
with plenty of room for discussion.

* location: Leipzig, Germany
* date: May 17 - 19, 2008
* local organizer: Johannes Waldmann, HTWK Leipzig

== Registration/Program ==

Please register by writing your name here
and the title of the talk you want to give,
or the topic you want to discuss.
(Feel free to create wiki pages for your topic, and link from here.)

* Johannes Waldmann, topics I'd like to see
** the present of Rainbow (give help to people who want to use this, may include some time for actual implementation/hacking)
** future of Rainbow (what has become of the plans we made http://color.loria.fr/workshop.html)

* Christian Sternagel, (Topic: TBA)

* Adam Koprowski, (topic: TBA)

* René Thiemann, topics to present (in combination with other colleagues from Innsbruck) and discuss
** presentation of (fixed) details on upcoming termination competition (TC)
** discussion of TC-details that have to be fixed by the community

* Frederic Blanqui. I can present the current state of Rainbow and CoLoR.

== Local Organization ==

Details will be fixed soon. Vote here! (Just mark with "X")

=== Options for location ===

* external conference facility (e.g. http://www.mediencampus-villa-ida.de/ ,rent would be 150 EUR per day), on-site restaurant/catering (additional cost)

* (XXX) classroom at HTWK (e.g. "Lipsius-Bau" on that map: http://www.htwk-leipzig.de/hochsch/lageplan.pdf , low or no cost) , self-catering (several small restaurants nearby)

=== Options for date/time ===

* workshop start: Saturday
** (XX) morning (9 a.m.) or
** (X) noon (1 p.m.)
* Workshop Dinner (Sunday), booking a table at some restaurant
** in the city center
** (XX) outskirts (may include walk or tram ride)
* workshop end: Monday
** (XX) noon (1 p.m.) or
** afternoon (5 p.m.)

== Accomodation ==

You'll find plenty of hotels of all price ranges through the usual
[http://maps.google.de/maps?f=l&hl=de&geocode=&q=hotel&near=Leipzig+Gustav+Freytag+Stra%C3%9Fe&sll=51.315754,12.37009&sspn=0.039108,0.076733&ie=UTF8&ll=51.313823,12.37421&spn=0.019555,0.038366&z=15 search engines]

HTWK is at Karl-Liebknecht-Straße/Richard-Lehmann-Straße.

(note: Hotel Seeblick is not a hotel. And there is no Lake.)

== Adjacent event(s) ==

Note that WScT08 is right after
[http://www.orchid.inf.tu-dresden.de/gdp/wata08/ WATA08 Dresden].
(There will even be some termination talks at WATA.)
Travel from Dresden to Leipzig is easy (one hour by train).
Dresden is a major tourist attraction.

What domain name?

2008-03-31T14:08:02Z

Blanqui:

We want to have a domain name for this web site.
What is your preference? Vote here

* termination-portal.org

* termination-live.org (by analogy to satlive.org)

* termination.at

or extend the list (but check that the name is free).
(everything like termination.* seems already taken)

Peter: I like termination-portal as it is descriptive. (Carsten Otto thinks the same.)

Carsten Fuhs: Another proposal might be <i>termination.at</i> (still free according to whois). The name is quite catchy and short, and I do not think that using a "national" domain name (here: Austria) would be a big problem. Does anyone know how hard it is to get an .at-domain?

F. Blanqui: I vote for termination-portal.org.

People:Frederic Blanqui

2008-03-30T13:05:50Z

Blanqui: New page: <!-- Please fill in the data so that you can be added to some default categories and a simple user page can be created. You may extend that user page yourself after th...

{{Person
|firstname=Frederic
|middlenames=
|lastname=Blanqui
|titles=
|email=
|homepage=http://www.loria.fr/~blanqui/
|country=France
|university=INRIA
|department=
|role=Researcher 
}}

Tools:Rainbow

2008-03-30T13:04:51Z

Blanqui: added rainbow

{{Tool
|shortname=Rainbow
|longname=Termination proof certifier
|homepage=http://color.loria.fr/
|country=France and The Netherlands
|university=INRIA and Eindhoven University of Technology
|developers=Frederic Blanqui and Adam Koprowski
}}

Tools:CoLoR

2008-03-30T13:02:47Z

Blanqui: more on universities

{{Tool
|shortname=CoLoR
|longname=Coq Library on Termination and Rewriting
|homepage=http://color.loria.fr/
|country=France and The Netherlands
|university=INRIA and Eindhoven University of Technology
|developers=Frederic Blanqui and Adam Koprowski
}}

Tools:CoLoR

2008-03-30T12:59:13Z

Blanqui: added CoLoR

{{Tool
|shortname=CoLoR
|longname=Coq Library on Termination and Rewriting
|homepage=http://color.loria.fr/
|country=France
|university=INRIA
|developers=Blanqui,Koprowski
}}