Welcome to TiddlyWiki created by Jeremy Ruston, Copyright © 2007 UnaMesa Association
Background: #fff
Foreground: #000
PrimaryPale: #8cf
PrimaryLight: #18f
PrimaryMid: #04b
PrimaryDark: #014
SecondaryPale: #ffc
SecondaryLight: #fe8
SecondaryMid: #db4
SecondaryDark: #841
TertiaryPale: #eee
TertiaryLight: #ccc
TertiaryMid: #999
TertiaryDark: #666
Error: #f88
/*{{{*/
body {background:[[ColorPalette::Background]]; color:[[ColorPalette::Foreground]];}
a {color:[[ColorPalette::PrimaryMid]];}
a:hover {background-color:[[ColorPalette::PrimaryMid]]; color:[[ColorPalette::Background]];}
a img {border:0;}
h1,h2,h3,h4,h5,h6 {color:[[ColorPalette::SecondaryDark]]; background:transparent;}
h1 {border-bottom:2px solid [[ColorPalette::TertiaryLight]];}
h2,h3 {border-bottom:1px solid [[ColorPalette::TertiaryLight]];}
.button {color:[[ColorPalette::PrimaryDark]]; border:1px solid [[ColorPalette::Background]];}
.button:hover {color:[[ColorPalette::PrimaryDark]]; background:[[ColorPalette::SecondaryLight]]; border-color:[[ColorPalette::SecondaryMid]];}
.button:active {color:[[ColorPalette::Background]]; background:[[ColorPalette::SecondaryMid]]; border:1px solid [[ColorPalette::SecondaryDark]];}
.header {background:[[ColorPalette::PrimaryMid]];}
.headerShadow {color:[[ColorPalette::Foreground]];}
.headerShadow a {font-weight:normal; color:[[ColorPalette::Foreground]];}
.headerForeground {color:[[ColorPalette::Background]];}
.headerForeground a {font-weight:normal; color:[[ColorPalette::PrimaryPale]];}
.tabSelected{color:[[ColorPalette::PrimaryDark]];
background:[[ColorPalette::TertiaryPale]];
border-left:1px solid [[ColorPalette::TertiaryLight]];
border-top:1px solid [[ColorPalette::TertiaryLight]];
border-right:1px solid [[ColorPalette::TertiaryLight]];
}
.tabUnselected {color:[[ColorPalette::Background]]; background:[[ColorPalette::TertiaryMid]];}
.tabContents {color:[[ColorPalette::PrimaryDark]]; background:[[ColorPalette::TertiaryPale]]; border:1px solid [[ColorPalette::TertiaryLight]];}
.tabContents .button {border:0;}
#sidebar {}
#sidebarOptions input {border:1px solid [[ColorPalette::PrimaryMid]];}
#sidebarOptions .sliderPanel {background:[[ColorPalette::PrimaryPale]];}
#sidebarOptions .sliderPanel a {border:none;color:[[ColorPalette::PrimaryMid]];}
#sidebarOptions .sliderPanel a:hover {color:[[ColorPalette::Background]]; background:[[ColorPalette::PrimaryMid]];}
#sidebarOptions .sliderPanel a:active {color:[[ColorPalette::PrimaryMid]]; background:[[ColorPalette::Background]];}
.wizard {background:[[ColorPalette::PrimaryPale]]; border:1px solid [[ColorPalette::PrimaryMid]];}
.wizard h1 {color:[[ColorPalette::PrimaryDark]]; border:none;}
.wizard h2 {color:[[ColorPalette::Foreground]]; border:none;}
.wizardStep {background:[[ColorPalette::Background]]; color:[[ColorPalette::Foreground]];
border:1px solid [[ColorPalette::PrimaryMid]];}
.wizardStep.wizardStepDone {background:[[ColorPalette::TertiaryLight]];}
.wizardFooter {background:[[ColorPalette::PrimaryPale]];}
.wizardFooter .status {background:[[ColorPalette::PrimaryDark]]; color:[[ColorPalette::Background]];}
.wizard .button {color:[[ColorPalette::Foreground]]; background:[[ColorPalette::SecondaryLight]]; border: 1px solid;
border-color:[[ColorPalette::SecondaryPale]] [[ColorPalette::SecondaryDark]] [[ColorPalette::SecondaryDark]] [[ColorPalette::SecondaryPale]];}
.wizard .button:hover {color:[[ColorPalette::Foreground]]; background:[[ColorPalette::Background]];}
.wizard .button:active {color:[[ColorPalette::Background]]; background:[[ColorPalette::Foreground]]; border: 1px solid;
border-color:[[ColorPalette::PrimaryDark]] [[ColorPalette::PrimaryPale]] [[ColorPalette::PrimaryPale]] [[ColorPalette::PrimaryDark]];}
#messageArea {border:1px solid [[ColorPalette::SecondaryMid]]; background:[[ColorPalette::SecondaryLight]]; color:[[ColorPalette::Foreground]];}
#messageArea .button {color:[[ColorPalette::PrimaryMid]]; background:[[ColorPalette::SecondaryPale]]; border:none;}
.popupTiddler {background:[[ColorPalette::TertiaryPale]]; border:2px solid [[ColorPalette::TertiaryMid]];}
.popup {background:[[ColorPalette::TertiaryPale]]; color:[[ColorPalette::TertiaryDark]]; border-left:1px solid [[ColorPalette::TertiaryMid]]; border-top:1px solid [[ColorPalette::TertiaryMid]]; border-right:2px solid [[ColorPalette::TertiaryDark]]; border-bottom:2px solid [[ColorPalette::TertiaryDark]];}
.popup hr {color:[[ColorPalette::PrimaryDark]]; background:[[ColorPalette::PrimaryDark]]; border-bottom:1px;}
.popup li.disabled {color:[[ColorPalette::TertiaryMid]];}
.popup li a, .popup li a:visited {color:[[ColorPalette::Foreground]]; border: none;}
.popup li a:hover {background:[[ColorPalette::SecondaryLight]]; color:[[ColorPalette::Foreground]]; border: none;}
.popup li a:active {background:[[ColorPalette::SecondaryPale]]; color:[[ColorPalette::Foreground]]; border: none;}
.popupHighlight {background:[[ColorPalette::Background]]; color:[[ColorPalette::Foreground]];}
.listBreak div {border-bottom:1px solid [[ColorPalette::TertiaryDark]];}
.tiddler .defaultCommand {font-weight:bold;}
.shadow .title {color:[[ColorPalette::TertiaryDark]];}
.title {color:[[ColorPalette::SecondaryDark]];}
.subtitle {color:[[ColorPalette::TertiaryDark]];}
.toolbar {color:[[ColorPalette::PrimaryMid]];}
.toolbar a {color:[[ColorPalette::TertiaryLight]];}
.selected .toolbar a {color:[[ColorPalette::TertiaryMid]];}
.selected .toolbar a:hover {color:[[ColorPalette::Foreground]];}
.tagging, .tagged {border:1px solid [[ColorPalette::TertiaryPale]]; background-color:[[ColorPalette::TertiaryPale]];}
.selected .tagging, .selected .tagged {background-color:[[ColorPalette::TertiaryLight]]; border:1px solid [[ColorPalette::TertiaryMid]];}
.tagging .listTitle, .tagged .listTitle {color:[[ColorPalette::PrimaryDark]];}
.tagging .button, .tagged .button {border:none;}
.footer {color:[[ColorPalette::TertiaryLight]];}
.selected .footer {color:[[ColorPalette::TertiaryMid]];}
.sparkline {background:[[ColorPalette::PrimaryPale]]; border:0;}
.sparktick {background:[[ColorPalette::PrimaryDark]];}
.error, .errorButton {color:[[ColorPalette::Foreground]]; background:[[ColorPalette::Error]];}
.warning {color:[[ColorPalette::Foreground]]; background:[[ColorPalette::SecondaryPale]];}
.lowlight {background:[[ColorPalette::TertiaryLight]];}
.zoomer {background:none; color:[[ColorPalette::TertiaryMid]]; border:3px solid [[ColorPalette::TertiaryMid]];}
.imageLink, #displayArea .imageLink {background:transparent;}
.annotation {background:[[ColorPalette::SecondaryLight]]; color:[[ColorPalette::Foreground]]; border:2px solid [[ColorPalette::SecondaryMid]];}
.viewer .listTitle {list-style-type:none; margin-left:-2em;}
.viewer .button {border:1px solid [[ColorPalette::SecondaryMid]];}
.viewer blockquote {border-left:3px solid [[ColorPalette::TertiaryDark]];}
.viewer table, table.twtable {border:2px solid [[ColorPalette::TertiaryDark]];}
.viewer th, .viewer thead td, .twtable th, .twtable thead td {background:[[ColorPalette::SecondaryMid]]; border:1px solid [[ColorPalette::TertiaryDark]]; color:[[ColorPalette::Background]];}
.viewer td, .viewer tr, .twtable td, .twtable tr {border:1px solid [[ColorPalette::TertiaryDark]];}
.viewer pre {border:1px solid [[ColorPalette::SecondaryLight]]; background:[[ColorPalette::SecondaryPale]];}
.viewer code {color:[[ColorPalette::SecondaryDark]];}
.viewer hr {border:0; border-top:dashed 1px [[ColorPalette::TertiaryDark]]; color:[[ColorPalette::TertiaryDark]];}
.highlight, .marked {background:[[ColorPalette::SecondaryLight]];}
.editor input {border:1px solid [[ColorPalette::PrimaryMid]];}
.editor textarea {border:1px solid [[ColorPalette::PrimaryMid]]; width:100%;}
.editorFooter {color:[[ColorPalette::TertiaryMid]];}
#backstageArea {background:[[ColorPalette::Foreground]]; color:[[ColorPalette::TertiaryMid]];}
#backstageArea a {background:[[ColorPalette::Foreground]]; color:[[ColorPalette::Background]]; border:none;}
#backstageArea a:hover {background:[[ColorPalette::SecondaryLight]]; color:[[ColorPalette::Foreground]]; }
#backstageArea a.backstageSelTab {background:[[ColorPalette::Background]]; color:[[ColorPalette::Foreground]];}
#backstageButton a {background:none; color:[[ColorPalette::Background]]; border:none;}
#backstageButton a:hover {background:[[ColorPalette::Foreground]]; color:[[ColorPalette::Background]]; border:none;}
#backstagePanel {background:[[ColorPalette::Background]]; border-color: [[ColorPalette::Background]] [[ColorPalette::TertiaryDark]] [[ColorPalette::TertiaryDark]] [[ColorPalette::TertiaryDark]];}
.backstagePanelFooter .button {border:none; color:[[ColorPalette::Background]];}
.backstagePanelFooter .button:hover {color:[[ColorPalette::Foreground]];}
#backstageCloak {background:[[ColorPalette::Foreground]]; opacity:0.6; filter:'alpha(opacity:60)';}
/*}}}*/
/*{{{*/
* html .tiddler {height:1%;}
body {font-size:.75em; font-family:arial,helvetica; margin:0; padding:0;}
h1,h2,h3,h4,h5,h6 {font-weight:bold; text-decoration:none;}
h1,h2,h3 {padding-bottom:1px; margin-top:1.2em;margin-bottom:0.3em;}
h4,h5,h6 {margin-top:1em;}
h1 {font-size:1.35em;}
h2 {font-size:1.25em;}
h3 {font-size:1.1em;}
h4 {font-size:1em;}
h5 {font-size:.9em;}
hr {height:1px;}
a {text-decoration:none;}
dt {font-weight:bold;}
ol {list-style-type:decimal;}
ol ol {list-style-type:lower-alpha;}
ol ol ol {list-style-type:lower-roman;}
ol ol ol ol {list-style-type:decimal;}
ol ol ol ol ol {list-style-type:lower-alpha;}
ol ol ol ol ol ol {list-style-type:lower-roman;}
ol ol ol ol ol ol ol {list-style-type:decimal;}
.txtOptionInput {width:11em;}
#contentWrapper .chkOptionInput {border:0;}
.externalLink {text-decoration:underline;}
.indent {margin-left:3em;}
.outdent {margin-left:3em; text-indent:-3em;}
code.escaped {white-space:nowrap;}
.tiddlyLinkExisting {font-weight:bold;}
.tiddlyLinkNonExisting {font-style:italic;}
/* the 'a' is required for IE, otherwise it renders the whole tiddler in bold */
a.tiddlyLinkNonExisting.shadow {font-weight:bold;}
#mainMenu .tiddlyLinkExisting,
#mainMenu .tiddlyLinkNonExisting,
#sidebarTabs .tiddlyLinkNonExisting {font-weight:normal; font-style:normal;}
#sidebarTabs .tiddlyLinkExisting {font-weight:bold; font-style:normal;}
.header {position:relative;}
.header a:hover {background:transparent;}
.headerShadow {position:relative; padding:4.5em 0em 1em 1em; left:-1px; top:-1px;}
.headerForeground {position:absolute; padding:4.5em 0em 1em 1em; left:0px; top:0px;}
.siteTitle {font-size:3em;}
.siteSubtitle {font-size:1.2em;}
#mainMenu {position:absolute; left:0; width:10em; text-align:right; line-height:1.6em; padding:1.5em 0.5em 0.5em 0.5em; font-size:1.1em;}
#sidebar {position:absolute; right:3px; width:16em; font-size:.9em;}
#sidebarOptions {padding-top:0.3em;}
#sidebarOptions a {margin:0em 0.2em; padding:0.2em 0.3em; display:block;}
#sidebarOptions input {margin:0.4em 0.5em;}
#sidebarOptions .sliderPanel {margin-left:1em; padding:0.5em; font-size:.85em;}
#sidebarOptions .sliderPanel a {font-weight:bold; display:inline; padding:0;}
#sidebarOptions .sliderPanel input {margin:0 0 .3em 0;}
#sidebarTabs .tabContents {width:15em; overflow:hidden;}
.wizard {padding:0.1em 1em 0em 2em;}
.wizard h1 {font-size:2em; font-weight:bold; background:none; padding:0em 0em 0em 0em; margin:0.4em 0em 0.2em 0em;}
.wizard h2 {font-size:1.2em; font-weight:bold; background:none; padding:0em 0em 0em 0em; margin:0.4em 0em 0.2em 0em;}
.wizardStep {padding:1em 1em 1em 1em;}
.wizard .button {margin:0.5em 0em 0em 0em; font-size:1.2em;}
.wizardFooter {padding:0.8em 0.4em 0.8em 0em;}
.wizardFooter .status {padding:0em 0.4em 0em 0.4em; margin-left:1em;}
.wizard .button {padding:0.1em 0.2em 0.1em 0.2em;}
#messageArea {position:fixed; top:2em; right:0em; margin:0.5em; padding:0.5em; z-index:2000; _position:absolute;}
.messageToolbar {display:block; text-align:right; padding:0.2em 0.2em 0.2em 0.2em;}
#messageArea a {text-decoration:underline;}
.tiddlerPopupButton {padding:0.2em 0.2em 0.2em 0.2em;}
.popupTiddler {position: absolute; z-index:300; padding:1em 1em 1em 1em; margin:0;}
.popup {position:absolute; z-index:300; font-size:.9em; padding:0; list-style:none; margin:0;}
.popup .popupMessage {padding:0.4em;}
.popup hr {display:block; height:1px; width:auto; padding:0; margin:0.2em 0em;}
.popup li.disabled {padding:0.4em;}
.popup li a {display:block; padding:0.4em; font-weight:normal; cursor:pointer;}
.listBreak {font-size:1px; line-height:1px;}
.listBreak div {margin:2px 0;}
.tabset {padding:1em 0em 0em 0.5em;}
.tab {margin:0em 0em 0em 0.25em; padding:2px;}
.tabContents {padding:0.5em;}
.tabContents ul, .tabContents ol {margin:0; padding:0;}
.txtMainTab .tabContents li {list-style:none;}
.tabContents li.listLink { margin-left:.75em;}
#contentWrapper {display:block;}
#splashScreen {display:none;}
#displayArea {margin:1em 17em 0em 14em;}
.toolbar {text-align:right; font-size:.9em;}
.tiddler {padding:1em 1em 0em 1em;}
.missing .viewer,.missing .title {font-style:italic;}
.title {font-size:1.6em; font-weight:bold;}
.missing .subtitle {display:none;}
.subtitle {font-size:1.1em;}
.tiddler .button {padding:0.2em 0.4em;}
.tagging {margin:0.5em 0.5em 0.5em 0; float:left; display:none;}
.isTag .tagging {display:block;}
.tagged {margin:0.5em; float:right;}
.tagging, .tagged {font-size:0.9em; padding:0.25em;}
.tagging ul, .tagged ul {list-style:none; margin:0.25em; padding:0;}
.tagClear {clear:both;}
.footer {font-size:.9em;}
.footer li {display:inline;}
.annotation {padding:0.5em; margin:0.5em;}
* html .viewer pre {width:99%; padding:0 0 1em 0;}
.viewer {line-height:1.4em; padding-top:0.5em;}
.viewer .button {margin:0em 0.25em; padding:0em 0.25em;}
.viewer blockquote {line-height:1.5em; padding-left:0.8em;margin-left:2.5em;}
.viewer ul, .viewer ol {margin-left:0.5em; padding-left:1.5em;}
.viewer table, table.twtable {border-collapse:collapse; margin:0.8em 1.0em;}
.viewer th, .viewer td, .viewer tr,.viewer caption,.twtable th, .twtable td, .twtable tr,.twtable caption {padding:3px;}
table.listView {font-size:0.85em; margin:0.8em 1.0em;}
table.listView th, table.listView td, table.listView tr {padding:0px 3px 0px 3px;}
.viewer pre {padding:0.5em; margin-left:0.5em; font-size:1.2em; line-height:1.4em; overflow:auto;}
.viewer code {font-size:1.2em; line-height:1.4em;}
.editor {font-size:1.1em;}
.editor input, .editor textarea {display:block; width:100%; font:inherit;}
.editorFooter {padding:0.25em 0em; font-size:.9em;}
.editorFooter .button {padding-top:0px; padding-bottom:0px;}
.fieldsetFix {border:0; padding:0; margin:1px 0px 1px 0px;}
.sparkline {line-height:1em;}
.sparktick {outline:0;}
.zoomer {font-size:1.1em; position:absolute; overflow:hidden;}
.zoomer div {padding:1em;}
* html #backstage {width:99%;}
* html #backstageArea {width:99%;}
#backstageArea {display:none; position:relative; overflow: hidden; z-index:150; padding:0.3em 0.5em 0.3em 0.5em;}
#backstageToolbar {position:relative;}
#backstageArea a {font-weight:bold; margin-left:0.5em; padding:0.3em 0.5em 0.3em 0.5em;}
#backstageButton {display:none; position:absolute; z-index:175; top:0em; right:0em;}
#backstageButton a {padding:0.1em 0.4em 0.1em 0.4em; margin:0.1em 0.1em 0.1em 0.1em;}
#backstage {position:relative; width:100%; z-index:50;}
#backstagePanel {display:none; z-index:100; position:absolute; margin:0em 3em 0em 3em; padding:1em 1em 1em 1em;}
.backstagePanelFooter {padding-top:0.2em; float:right;}
.backstagePanelFooter a {padding:0.2em 0.4em 0.2em 0.4em;}
#backstageCloak {display:none; z-index:20; position:absolute; width:100%; height:100px;}
.whenBackstage {display:none;}
.backstageVisible .whenBackstage {display:block;}
/*}}}*/
/***
StyleSheet for use when a translation requires any css style changes.
This StyleSheet can be used directly by languages such as Chinese, Japanese and Korean which use a logographic writing system and need larger font sizes.
***/
/*{{{*/
body {font-size:0.8em;}
#sidebarOptions {font-size:1.05em;}
#sidebarOptions a {font-style:normal;}
#sidebarOptions .sliderPanel {font-size:0.95em;}
.subtitle {font-size:0.8em;}
.viewer table.listView {font-size:0.95em;}
.htmlarea .toolbarHA table {border:1px solid ButtonFace; margin:0em 0em;}
/*}}}*/
/*{{{*/
@media print {
#mainMenu, #sidebar, #messageArea, .toolbar, #backstageButton, #backstageArea {display: none ! important;}
#displayArea {margin: 1em 1em 0em 1em;}
/* Fixes a feature in Firefox 1.5.0.2 where print preview displays the noscript content */
noscript {display:none;}
}
/*}}}*/
<!--{{{-->
<div class='header' macro='gradient vert [[ColorPalette::PrimaryLight]] [[ColorPalette::PrimaryMid]]'>
<div class='headerShadow'>
<span class='siteTitle' refresh='content' tiddler='SiteTitle'></span>
<span class='siteSubtitle' refresh='content' tiddler='SiteSubtitle'></span>
</div>
<div class='headerForeground'>
<span class='siteTitle' refresh='content' tiddler='SiteTitle'></span>
<span class='siteSubtitle' refresh='content' tiddler='SiteSubtitle'></span>
</div>
</div>
<div id='mainMenu' refresh='content' tiddler='MainMenu'></div>
<div id='sidebar'>
<div id='sidebarOptions' refresh='content' tiddler='SideBarOptions'></div>
<div id='sidebarTabs' refresh='content' force='true' tiddler='SideBarTabs'></div>
</div>
<div id='displayArea'>
<div id='messageArea'></div>
<div id='tiddlerDisplay'></div>
</div>
<!--}}}-->
<!--{{{-->
<div class='toolbar' macro='toolbar closeTiddler closeOthers +editTiddler > fields syncing permalink references jump'></div>
<div class='title' macro='view title'></div>
<div class='subtitle'><span macro='view modifier link'></span>, <span macro='view modified date'></span> (<span macro='message views.wikified.createdPrompt'></span> <span macro='view created date'></span>)</div>
<div class='tagging' macro='tagging'></div>
<div class='tagged' macro='tags'></div>
<div class='viewer' macro='view text wikified'></div>
<div class='tagClear'></div>
<!--}}}-->
<!--{{{-->
<div class='toolbar' macro='toolbar +saveTiddler -cancelTiddler deleteTiddler'></div>
<div class='title' macro='view title'></div>
<div class='editor' macro='edit title'></div>
<div macro='annotations'></div>
<div class='editor' macro='edit text'></div>
<div class='editor' macro='edit tags'></div><div class='editorFooter'><span macro='message views.editor.tagPrompt'></span><span macro='tagChooser'></span></div>
<!--}}}-->
To get started with this blank TiddlyWiki, you'll need to modify the following tiddlers:
* SiteTitle & SiteSubtitle: The title and subtitle of the site, as shown above (after saving, they will also appear in the browser title bar)
* MainMenu: The menu (usually on the left)
* DefaultTiddlers: Contains the names of the tiddlers that you want to appear when the TiddlyWiki is opened
You'll also need to enter your username for signing your edits: <<option txtUserName>>
These InterfaceOptions for customising TiddlyWiki are saved in your browser
Your username for signing your edits. Write it as a WikiWord (eg JoeBloggs)
<<option txtUserName>>
<<option chkSaveBackups>> SaveBackups
<<option chkAutoSave>> AutoSave
<<option chkRegExpSearch>> RegExpSearch
<<option chkCaseSensitiveSearch>> CaseSensitiveSearch
<<option chkAnimate>> EnableAnimations
----
Also see AdvancedOptions
Institution: ~Tel-Aviv Academic College
(joint work with Neil Jones and Lars Kristiansen)
Title: Automatic Certification of Complexity for Programs with ~For-Loops
Abstract: We present a new method for inferring complexity bounds for imperative programs with for-loops. The method is targeted at programs computing with nonnegative integers and the properties handled are: polynomial (or linear) boundedness of values; and similarly for the running time.
!!!Purpose and scope of the meeting
The workshop is intended to be a forum for researchers interested in ICC to discuss recent developments and open issues. It will be open to contributions on various aspects of ICC including (but not exclusively):
* characterizations of various complexity classes,
* logical systems for ICC,
* semantic and interpretation-based methods for complexity,
* types for controlling complexity,
* linear logic,
* semantics of complexity-bounded computation,
* function algebras, subrecursion.
!!!Talk proposal
/% If you intend to give a talk, just send us by email the following informations before December 21.
%/ It is now closed. Thank you for your proposals.
We will notify the acceptance and communicate the list of talks in January 2008.
/%
Talk proposal: send it to //Paulin.Jacobedenaurois@lipn.univ-paris13.fr//
----------------------------------------------------------------------
First name:
Last name:
Institution:
Title:
Short abstract:
----------------------------------------------------------------------
%/
Institution: PPS / CNRS Université Paris 7
[[Slides|slides/slides_Mazza_wicc08.pdf]]
Title: Linear Logic by Levels and Bounded Time Complexity
Abstract : We present a work dealing with the characterization of elementary and deterministic polynomial time computation in linear logic through the proofs-as-programs correspondence. Girard's seminal results, concerning elementary and light linear logic, use a principle called stratification" to ensure the complexity bound on the cut-elimination procedure. Here, we propose a more flexible control principle, that of "indexing", which allows us to extend Girard's systems while keeping the same complexity properties. A consequence of the higher flexibility of indexing with respect to stratification is the absence of boxes for handling the § modality. We finally propose a variant of our polytime system in which the § modality is only allowed on atoms, and which may thus serve as a basis for developing lambda-calculus type assignment systems with more efficient typing algorithms than existing ones.
Institution: LORIA Nancy
(Joint work with Michele Pagani, PPS / CNRS Université Paris 7)
[[Slides|slides/slides_De_Carvalho_wicc08.pdf]]
Title: A semantic measure of the execution time in Linear Logic
Abstract: We give a semantic account of the execution time (i.e. the number of cut-elimination steps leading to the normal form) of an untyped MELL (proof-)net. We first prove that: 1) a net is head-normalizable (i.e. normalizable at depth 0) if and only if its interpretation in the multiset based relational semantics is not empty and 2) a net is normalizable if and only if its exhaustive interpretation (a suitable restriction of its interpretation) is not empty. We then define a size on every experiment of a net, and we precisely relate the number of cut-elimination steps of every stratified reduction sequence to the size of a particular experiment.
Finally, we give a semantic measure of execution time: we prove that we can compute the number of cut-elimination steps leading to a cut free normal form of the net obtained by connecting two cut free nets by means of a cut link, from the interpretations of the two cut free nets. These results are inspired by similar ones obtained by Daniel de Carvalho for the (untyped) lambda-calculus.
Institution: Nancy Universités - Loria - UHP
[[Slides|slides/slides_Hainry_wicc08.pdf]]
Title: Subrecursion in recursive analysis
Abstract: Recursive analysis is a well established framework for computing over real numbers. It allows to describe computability on real numbers but also smaller classes of computable functions such as elementary functions, polynomial-time computable functions... Those classes of functions however are described machine-dependently. This talk will present some function algebras that characterize various classes of recursive and sub-recursive function (elementary functions, Grzegorczyk's classes) for recursive analysis in a totally machine-independent manner using natural and hopefully simple mathematical operators.
The workshop will take place in Amphithéâtre Copernic (Very close to the entrance of //Institut Galilée// - labelled G on the campus map).
The ''slides'' are joined to each abstract (there is also a [[big .tgz file|all_slides_wicc08.tgz]] of all slides - 41Mo). Thanks to the speakers.
<html>
<a href="javascript:void(0)" onclick="story.closeAllTiddlers();story.displayTiddlers(null,['Event Programme','James Royer','Norman Danner','Jean-Yves Marion','Harry Mairson','Stefan Schimanski','Damiano Mazza','Isabel Oitavem','Reinhard Kahle','Vittoria Cozza','Simona Ronchi della Rocca','Marco Gaboardi','Ulrich Schoepp','Olivier Laurent','Amir Ben-Amram','Guillaume Bonfante','Olha Sharavska','Romain Péchoux','Emmanuel Hainry','Kazushige Terui','Daniel De Carvalho','Richard McKinley','Luca Roversi','Luca Vercelli','Ugo Dal Lago'])">Click here to display (at the bottom of the page) all the abstracts</a>, click on a day in the table to display the corresponding abstracts, and
<a href="javascript:void(0)" onclick="story.closeAllTiddlers();story.displayTiddlers(null,['Event Programme'])">click here to close all the abstracts.</a></html>
| || <html><a href="javascript:void(0)" onclick="story.closeAllTiddlers();story.displayTiddlers(null,['Event Programme','James Royer','Norman Danner','Jean-Yves Marion','Harry Mairson','Stefan Schimanski','Damiano Mazza','Isabel Oitavem','Reinhard Kahle','Vittoria Cozza'])">Monday</a></html> || <html><a href="javascript:void(0)" onclick="story.closeAllTiddlers();story.displayTiddlers(null,['Event Programme','Simona Ronchi della Rocca','Marco Gaboardi','Ulrich Schoepp','Olivier Laurent','Amir Ben-Amram','Guillaume Bonfante','Olha Sharavska','Romain Péchoux','Emmanuel Hainry'])">Tuesday</a></html> || <html><a href="javascript:void(0)" onclick="story.closeAllTiddlers();story.displayTiddlers(null,['Event Programme','Kazushige Terui','Daniel De Carvalho','Richard McKinley','Luca Roversi','Luca Vercelli','Ugo Dal Lago'])">Wednesday</a></html> |
| || || || |
|bgcolor:#04b;color:#fff; 9h30 10h00 || //Welcome// || ||bgcolor:#abf; [[Kazushige Terui]] On space efficiency of Krivine's abstract machine and pointer abstract machine |
|bgcolor:#04b;color:#fff; 10h00 10h30 ||bgcolor:#abf; [[Lars Krisitiansen|http://lipn.fr/nocost/IMG/pdf/Kristiansen_Wicc.pdf]] Implicit Characterisations of Complexity Classes and Recursion in Higher Types ||bgcolor:#abf; [[Simona Ronchi della Rocca]] Soft Linear Logic and Polynomial Complexity classes ||bgcolor:#abf; [[Daniel De Carvalho]] A semantic measure of the execution time in Linear Logic |
|bgcolor:#04b;color:#fff; 10h30 11h00 ||bgcolor:#abf; Lars Krisitiansen - //Invited speaker// ||bgcolor:#abf; Simona Ronchi della Rocca - //Invited speaker// ||bgcolor:#abf; [[Richard McKinley]]<br> Soft Linear Set Theory |
|bgcolor:#04b;color:#fff; 11h00 11h30 || //Coffee Break// || //Coffee Break// || //Coffee Break// |
|bgcolor:#04b;color:#fff; 11h30 12h00 ||bgcolor:#abf; [[James Royer]]<br> Affine Tiered Recursion: Semantics and Pragmatic. I ||bgcolor:#abf; [[Marco Gaboardi]]<br> Towards a soft logic for PSPACE ||bgcolor:#abf; [[Luca Roversi]]<br> Weak Affine Light Logic |
|bgcolor:#04b;color:#fff; 12h00 12h30 ||bgcolor:#abf; [[Norman Danner]]<br> Affine Tiered Recursion: Semantics and Pragmatics. II ||bgcolor:#abf; [[Ulrich Schoepp]] Stratified Bounded Affine Logic for Logarithmic Space ||bgcolor:#abf; [[Luca Vercelli]]<br> IRSS |
|bgcolor:#04b;color:#fff; 12h30 13h00 ||bgcolor:#abf; [[Jean-Yves Marion]]<br> How to make small jumps ||bgcolor:#abf; [[Olivier Laurent]]<br> Game Model for Time Analsysis in Linear Logic ||bgcolor:#abf; [[Ugo Dal Lago]]<br> Quantum Implicit Computational Complexity |
|bgcolor:#04b;color:#fff; 13h00 - || //Lunch// || //Lunch// || //Lunch// |
|bgcolor:#04b;color:#fff; - 14h30 || //Lunch// || //Lunch// || //Lunch// |
|bgcolor:#04b;color:#fff; 14h30 15h00 ||bgcolor:#abf; [[Harry Mairson]]<br> Linear Logic and the Complexity of Control Flow Analysis ||bgcolor:#abf; [[Amir Ben-Amram]]<br> Automatic Certification of Complexity for Programs with ~For-Loops || |
|bgcolor:#04b;color:#fff; 15h00 15h30 ||bgcolor:#abf; [[Stefan Schimanski]]<br> A Light Linear T ||bgcolor:#abf; [[Guillaume Bonfante]]<br> Polynomial interpretations: the real role of reals || |
|bgcolor:#04b;color:#fff; 15h30 16h00 ||bgcolor:#abf; [[Damiano Mazza]]<br> Linear Logic by Levels and Bounded Time Complexity ||bgcolor:#abf; [[Olha Sharavska]] A Polynomial ~Size-Aware Type System with Decidable Type Inference || |
|bgcolor:#04b;color:#fff; 16h00 16h30 || //Coffee Break// || //Coffee Break// || |
|bgcolor:#04b;color:#fff; 16h30 17h00 ||bgcolor:#abf; [[Isabel Oitavem]]<br> A recursion-theoretic approach to NP ||bgcolor:#abf; [[Romain Péchoux]]<br> On the complexity of object oriented programs || |
|bgcolor:#04b;color:#fff; 17h00 17h30 ||bgcolor:#abf; [[Reinhard Kahle]]<br> Recursion schemata for NC^k ||bgcolor:#abf; [[Emmanuel Hainry]]<br> Subrecursion in recursive analysis || |
|bgcolor:#04b;color:#fff; 17h30 18h00 ||bgcolor:#abf; [[Vittoria Cozza]]<br> Feasible ICC C and its Harmonization with the Provable Hierarchy || || |
<html>
First name:<br>
<input name="prenom" value="" type=text/><br>
Name:<br>
<input name="nom" value="" type=text/><br>
Email:<br>
<input name="email" value="" type=text/><br>
Institution:<br>
<input name="institution" value="" type=text/><br>
<br>
Participation :
<input name="jour1" type=checkbox />Feb. 11
<input name="jour2" type=checkbox />Feb. 12
<input name="vegan" type=checkbox />Vegetarian<br>
<br>
<input name=btnSubmit type=submit />
<input name=btnReset type=reset />
</html>
Institution: LORIA Nancy
[[Slides|slides/slides_Bonfante_wicc08.pdf]] [[Movie|slides/movie_Bonfante_wicc08.pdf]]
Title: Polynomial interpretations: the real role of reals.
Abstract: We come back to the use of reals for polynomial interpretations. We show that they do not provide from an extensional point of view some larger class of functions. But they still may be of help for intentionality.
Institution: Brandeis University
[[Slides|slides/slides_Mairson_wicc08.pdf]]
Title: Linear Logic and the Complexity of Control Flow Analysis
Abstract: Control flow analysis (CFA) is a kind of static program analysis performed by compilers, where the answers to questions like "can call site X ever call procedure P?" or "can procedure P ever be called with argument A?" can be used to optimize code output by the compiler. Such questions can be answered exactly by Girard's geometry of interaction (~GoI), but in the interest of efficiency and time-bounded computation, control flow analysis computes a crude approximation to ~GoI, possibly including false positives.
Different versions of CFA are parameterized by their sensitivity to calling contexts, as represented by a contour -a sequence of k labels representing these contexts, analogous to Lévy's labelled lambda calculus. CFA with larger contours is designed to make the approximation more precise. A naive calculation shows that 0CFA (i.e., with k=0) can be solved in polynomial time, and kCFA (k>0, a constant) can be solved in exponential time. We show that these bounds are tight, namely, that the decision problem for 0CFA is ~PTIME- hard, and for kCFA is ~EXPTIME-hard. Each proof depends on fundamental insights about the linearity of programs. In both the linear and nonlinear case, contrasting simulations of the linear logic exponential are used in the analysis. The key idea is to take the approximation mechanism inherent in CFA, and exploit its crudeness to do real computation.
This is joint work with David Van Horn (Brandeis University).
''Talk proposal'': December 21th, 2007
''Registration'': January 21th, 2008
''Workshop'': February 11-12-13, 2008
//We will finish by mid-day on February 13th.//
Institution: ~FCT-UNL and CMAF - Universidade de Lisboa
[[Slides|slides/slides_Oitavem_wicc08.pdf]]
Title: A recursion-theoretic approach to NP
Abstract: In this talk we give an implicit characterization of the class NP, without using any minimization scheme. This is a purely recursion-theoretic formulation of NP.
Institution: Department of Electrical Eng. and Computer Science, Syracuse University
(Joint work with Norman Danner, Department of Mathematics and Computer Science, Wesleyan University)
Title: Affine Tiered Recursion: Semantics and Pragmatics
Abstract: ATR (for Affine Tiered Recursion) is a call-by-value version of PCF under a complexity-theoretically motivated type system. ATR programs characterize the usual polynomial-time computable functions at type-level 1 and the basic feasible functionals of Mehlhorn and Cook & Urquhart and type-level 2. Moreover, ATR can express a wide class of natural algorithms that use affine (one-use) recursion. For example, the ~ATR-versions of insertion and selection sort are close to the versions of those algorithms one would ordinarily write in a language like ML.
The type system comes in two parts: one that primarily restricts the sizes of values of expressions and a second that primarily restricts the time required to evaluate expressions. The size-restricted part is motivated by Bellantoni & Cook's and Leivant's implicit characterizations of polynomial-time. The time-restricting part is an affine version of Barber & Plotkin's Dual Intuitionistic Linear Logic (DILL).
ATR has two semantic interpretations: a denotational semantics and a time-complexity semantics. The denotational semantics results from "pruning" of the naive semantics for ATR to remove functions with growth rates that cause otherwise feasible recursions to go wrong. The time-complexity semantics is a model of ATR's run-time costs relative to a standard call-by-value abstract machine. This model provides a setting for complexity recurrences arising from ATR recursions, the solutions of which yield second-order polynomial time bounds. The time-complexity semantics is sound relative to the costs of evaluation on the abstract machine. The talk will discuss various facets of ATR, its type system, and its semantics, and discuss the rationale behind them. We will also discuss our work on developing a lazy (call-by-need) version of ATR.
References:
* N. Danner and J. S. Royer. Adventures in time and space. Logical Methods in Computer Science, 3(9), 2007.
* N. Danner and J. S. Royer. Time-complexity semantics for feasible affine recursions. In S. Cooper, B. Löwe, and A. Sorbi, editors, Computation in the Real World (Proceedings Computability in Europe 2007, Sienna), volume 4497 of Lecture Notes in Computer Science, Berlin, 2007. ~Springer-Verlag.
Institution: ~Loria-INPL
[[Slides|slides/slides_Marion_wicc08.pdf]]
Title : How to make small jumps
Abstract : Predicative analysis of recursion schema is a method to characterize complexity classes like the class of polynomial time functions. This analysis comes from the works of Bellantoni and Cook, and Leivant. Here, we refine predicative analysis by using a ramified Ackermann's construction of a non-primitive recursive function. We obtain an hierarchy of functions which characterizes exactly functions, which are computed in O(n^k) over register machine model of computation. Then, we are able to diagonalize using dependent types in order to obtain an exponential function.
Insitution: NII, Japan / LIPN, Villetaneuse
[[Slides|slides/slides_Terui_wicc08.pdf]]
Title: On space efficiency of Krivine's abstract machine and pointer abstract machine
Abstract: Our ultimate goal is to reconstruct the computational complexity theory fully based on logic and types. In this talk, we in particular discuss the space efficiency of evaluation in lambda calculus. It is well known that composition of two Turing machines (TM) has to be done in an interactive (game semantic) way when the space efficiency is at issue. This motivates us to study game-like evaluation mechanisms such as Krivine's Abstract Machine (KAM) and Pointer Abstract Machine (PAM) of ~Danos-Regnier (in addition to Geometry of Interaction, as done by Schoepp). We show that:
i) KAM space-efficiently simulates TM. Hence the space hierarchy theorem implies that there is no uniformly (i.e. for all terms) and significantly (eg. quadratically) more efficient way of evaluation than KAM.
ii) PAM evaluates simply typed terms up to rank 3 in PSPACE. This conforms to Schubert's theorem that normalization of rank 3 terms is ~PSPACE-complete. Hence there is no exponentially more efficient way of evaluation than PAM for rank 3 terms (unless PSPACE = LOGSPACE).
The workshop will take place in Amphithéâtre Copernic (Batiment de l'Institut Galilée - labelled G on the campus map) on the campus of Villetaneuse of the University of Paris 13, in the north surroundings of Paris (approx. 25 min for Gare du Nord).
You can find [[here|http://lipn.fr/planfac/?lang=uk]] and [[here|http://maps.google.fr/maps?f=q&hl=fr&geocode=&time=&date=&ttype=&q=WICC'08&sll=47.15984,2.988281&sspn=9.90606,19.643555&ie=UTF8&mrt=kmlkmz&ll=48.957031,2.341161&spn=0.018683,0.038366&t=h&z=15&om=1]] more details.
Social event is programmed on monday evening at the [[//brasserie Flo//|http://www.flobrasseries.com/brasseries/index.asp?brasserie=5]] (7, cour des Petites Ecuries = entrée par le 63 rue du Fg Saint Denis, 75010 Paris, Métro : Château d’eau, Tel : 01 47 70 13 59).
!!Hotels
Please find below a short list of hotels that we have selected for their convenience. All of them are located downtown Paris, relatively close to the "Gare du Nord" train station where you will find trains going to our university. In order to accommodate as many of you as possible, we have selected a rather large range of rates.
For those of you who prefer to look for themselves, we recommend the following [[hotel search engine|http://en.parisinfo.com/paris-hotels/hotels-1/]].
We advise you to select hotels around "gare du nord", or, alternatively, around "quartier latin" district where you will have a quick connection to gare du nord.
Please note that, when calling from abroad, you should dial (for instance) + 33 1 48 05 44 42 instead of 01 48 05 44 42.
---------------------------------------------------------------------------
28 EUR:
HOTEL DE VIENNE
43, rue de Malte, 75011 PARIS
tel: 01 48 05 44 42
fax: 01 48 05 44 26
mail: hoteldevienne@aol.com
www: http://www.hoteldevienne.com/
---------------------------------------------------------------------------
29 EUR:
HOTEL MODERNE DU TEMPLE
3, rue d'Aix, 75010 PARIS
tel: 01 42 08 09 04
fax: 01 42 41 72 17
mail : reception@hotelmodernedutemple.com
www: http://www.hotelmodernedutemple.com
---------------------------------------------------------------------------
40 EUR:
HOTEL JARRY
4, rue Jarry, 75010 PARIS
tel: 01 47 70 70 38
fax: 01 42 46 34 45
mail: hoteljarry@wanadoo.fr
www: http://www.hoteljarry.com
---------------------------------------------------------------------------
40 EUR:
HOTEL DE MILAN
17-19, rue de Saint Quentin, 75010 PARIS
tel: 01 40 37 88 50
fax: 01 46 07 89 48
mail: hdm@hoteldemilan.com
www: http://www.hoteldemilan.com
---------------------------------------------------------------------------
46 EUR:
HOTEL CAMBRAI
129 bis, boulevard Magenta, 75010 PARIS
tel: 01 48 78 32 13
fax: 01 48 78 43 55
mail: hotelcambrai@wanadoo.fr
www: http://www.hotel-cambrai.com
---------------------------------------------------------------------------
60 EUR:
HOTEL ARIS NORD
133, rue du Faubourg Saint Denis, 75010 PARIS
tel: 01 40 36 14 50
fax: 01 40 36 05 07
mail: info@aris-nord.com
www: http://www.aris-nord.com
---------------------------------------------------------------------------
68 EUR:
HOTEL D' ENGHIEN
52, rue d'Enghien, 75010 PARIS
tel: 01 47 70 56 49
fax: 01 45 23 04 52
mail: hoteld_enghien@yahoo.fr
www: http://www.hoteldenghien.com
---------------------------------------------------------------------------
68 EUR:
JARDINS DE PARIS REPUBLIQUE
30, rue Lucien Sampaix, 75010 PARIS
tel: 01.42.08.19.74
fax: 01.42.08.27.28
mail: republique@hotelsjardinsdeparis.com
www: http://www.hotelsjardinsdeparis.com
---------------------------------------------------------------------------
72 EUR:
HOTEL ~PARIS-LIEGE
36, rue de ~Saint-Quentin, 75010 PARIS
tel: 01 42 81 13 18
fax: 01 40 82 92 65
mail: liora@hotelparisliege.com
www: http://hotelparisliege.com/index.html
---------------------------------------------------------------------------
79 EUR:
IBIS JEMMAPES CANAL SAINT MARTIN
12, rue Louis Blanc, 75010 PARIS
tel: 01 42 01 21 21
fax: 01.42.08.21.40
mail: H0900@accor.com
www: http://www.ibishotel.com
---------------------------------------------------------------------------
79 EUR:
IBIS PARIS GARE DU NORD CHATEAU LANDON
197-199, rue La Fayette, 75010 PARIS
tel: 01 44 65 70 00
fax: 01 44 65 70 07
mail: h1823@accor.com
www: http://www.ibishotel.com
---------------------------------------------------------------------------
79 EUR:
IBIS PARIS GARE DU NORD LAFAYETTE
122, rue La Fayette, 75010 PARIS
tel: 01 45 23 27 27
fax: 01 42 46 73 79
mail: H0863@accor.com
www: http://www.ibishotel.com
---------------------------------------------------------------------------
91 EUR:
CAMPANILE GARE DU NORD
232, rue du Faubourg ~Saint-Martin, 75010 PARIS
tel: 01.40.34.38.38
fax: 01.40.34.38.50
mail: paris.garedunord@campanile.fr
www: http://www.campanile.fr
Institution: Dipartimento di Informatica,Torino
[[Slides|slides/slides_Roversi_wicc08.pdf]]
Title: Weak Affine Light Logic
Short abstract: Weak affine light typing (WALT) assigns light affine linear formulae as types to a subset of ?-terms typable in System F. WALT is poly-time sound: if a ?-term M has type in WALT,M can be evaluated with a polynomial cost in the dimension of the derivation that gives it a type. In particular, the evaluation can proceed under any strategy of a rewriting relation, obtained as a mix of both call-by-name/call-by-value ?-reductions. WALT is poly-time complete since it can represent any poly-time Turing machine.
WALT weakens, namely generalizes, the notion of stratification of deductions common to some Light Systems, which are those logical systems, derived from Linear logic, to characterize FP, the set of Polynomial functions. A weaker stratification allows to define a compositional embedding of the Quasi-linear fragment ~QlSRN of Safe recursion on notation (SRN) into WALT. ~QlSRN is SRN, which is a recursive-theoretical system characterizing FP, where the composition scheme is restricted to linear safe variables. So, the expressivity ofWALT is stronger, as compared to the known Light Systems that characterize FP. In particular, using the types, the embedding puts in evidence the stratification of normal and safe arguments hidden in ~QlSRN: the less an argument is impredicative, the deeper, in a formal, proof-theoretical sense, gets its representation in WALT.
Institution: Università di Torino
[[Slides|slides/slides_Vercelli_wicc08.pdf]]
Title: IRSS
Short abstract: This is a joint work with Luca Roversi. The focus of this work is what we call Intuitionistic, Relevantly Stratified, deductive Systems for polytime computations (IRSS). The goal is to show that theese systems enjoy the following properties:
(i) Polynomial soundness. The time of normalization of any derivation that belongs to a IRSS is polynomial in the size of the derivation.
(ii) The derivations of a IRSS are relevantly stratified. Namely, IRSS incorporates the design principles of LLL where dereliction is banned. Unconstrained weakening, though, is allowed.
(iii) IRSS are the largest set of deductive systems enjoying (i) and (ii).
We are not yet able to show (iii). However, thanks to (i) and (ii) we can prove that IRSS /strictly and soundly/ contains the known deductive systems, derived from (intuitionistic) versions of LLL: ILAL, DLAL, WALT. The inclusion is strict because IRSS are general enough to take under control normalization sequences that may led to exponential blow up. This poses IRSS as candidates to study how much intensionally expressive could be the systems derived from LL in the area of Implicit Computational Complexity.
[[Presentation]]
[[Important dates]]
[[Call for talk proposals]]
[[Event programme]]
[[Participants list]]
[[Registration (no fees)]]
[[Location and access]]
<html>
<a href="http://www-lipn.univ-paris13.fr" target="_blank">
<img src="http://www-lipn.univ-paris13.fr/image/LIPN_logo.jpg" width="100" alt="LIPN"></a>
</html>
Institution: Dipartimento di Informatica - Universita' di Torino
[[Slides|slides/slides_Gaboardi_wicc08.pdf]]
Title: Towards a soft logic for PSPACE
Abstract: In [~GaboardiMarionRonchiDellaRocca2008] we have introduced a type assignment system, named ~STA_B, correct and complete for PSPACE. ~STA_B is the first type system characterizing this class using the light logics approach. The expressiveness of ~STA_B depends on the use, both at type and language level, of Booleans constants managed additively. The soundness is obtained by giving a big step abstract machine that performs programs evaluation in polynomial space.
Starting from the ideas underlying ~STA_B, we would here exploit the proofs-as-programs correspondence to design a logic characterizing PSPACE. The logic system obtained by forgetting terms in ~STA_B is unsatisfactory. Boolean constants in a second order logic are redundant. Moreover, the ~STA_B evaluation mechanism does not directly translate in a standard cut elimination procedure. Starting from these considerations we discuss some possible solutions.
Institution: Department of Mathematics and Computer Science, Wesleyan University
(Joint work with James Royer , Department of Electrical Eng. and Computer Science, Syracuse University)
[[Slides|slides/slides_Danner_wicc08.pdf]]
Title: Affine Tiered Recursion: Semantics and Pragmatics
Abstract: ATR (for Affine Tiered Recursion) is a call-by-value version of PCF under a complexity-theoretically motivated type system. ATR programs characterize the usual polynomial-time computable functions at type-level 1 and the basic feasible functionals of Mehlhorn and Cook & Urquhart and type-level 2. Moreover, ATR can express a wide class of natural algorithms that use affine (one-use) recursion. For example, theATR-versions of insertion and selection sort are close to the versions of those algorithms one would ordinarily write in a language like ML.
The type system comes in two parts: one that primarily restricts the sizes of values of expressions and a second that primarily restricts the time required to evaluate expressions. The size-restricted part is motivated by Bellantoni & Cook's and Leivant's implicit characterizations of polynomial-time. The time-restricting part is an affine version of Barber & Plotkin's Dual Intuitionistic Linear Logic (DILL).
ATR has two semantic interpretations: a denotational semantics and a time-complexity semantics. The denotational semantics results from "pruning" of the naive semantics for ATR to remove functions with growth rates that cause otherwise feasible recursions to go wrong. The time-complexity semantics is a model of ATR's run-time costs relative to a standard call-by-value abstract machine. This model provides a setting for complexity recurrences arising from ATR recursions, the solutions of which yield second-order polynomial time bounds. The time-complexity semantics is sound relative to the costs of evaluation on the abstract machine. The talk will discuss various facets of ATR, its type system, and its semantics, and discuss the rationale behind them. We will also discuss our work on developing a lazy (call-by-need) version of ATR.
References:
* N. Danner and J. S. Royer. Adventures in time and space. Logical Methods in Computer Science, 3(9), 2007.
* N. Danner and J. S. Royer. Time-complexity semantics for feasible affine recursions. In S. Cooper, B. Löwe, and A. Sorbi, editors, Computation in the Real World (Proceedings Computability in Europe 2007, Sienna), volume 4497 of Lecture Notes in Computer Science, Berlin, 2007. ~Springer-Verlag.
Institution: Institute for Computing and Information Sciences, Radboud University Nijmegen
Joint work with Marko Van Eekelen, Institute for Computing and Information Sciences, Radboud University Nijmegen)
[[Slides|slides/slides_Sharavska_wicc08.pdf]]
Title: A Polynomial ~Size-Aware Type System with Decidable Type Inference.
Abstract: We propose a static size analysis procedure that combines term-rewriting and type checking to automatically obtain output-on-input size dependencies for first-order functions. Attention is restricted to functions for which the size of the result is strictly polynomial, not necessarily monotonous, in the sizes of the arguments. To infer a size dependency, the procedure generates hypotheses for increasing degrees of polynomials. For each degree, to define a hypothetical polynomial one needs to know its values on a finite collection of points (subject to some geometrical condition). To compute the value of a size polynomial in a certain point we use a term-rewriting system generated by a standard size-annotations inference procedure.
We propose a stopping criterion for type inference. This criterion is based upon the characteristics of the term-rewriting system. The criterion makes type inference decidable. Completeness of this type inference with respect to type checking is still an open problem, however.
Institution: PPS CNRS / Université Paris 7
(Joint work with Ugo Dal Lago, Università di Bologna)
[[Slides|slides/slides_Laurent_wicc08.pdf]]
Title: Game Model for Time Analsysis in Linear Logic
Abstract : We present a game model allowing to analyze reduction length for proofs of MELL. This gives a compositional view of the geometry of interaction framework introduced by Dal Lago. In our model the time measure is given by means of slots, as introduced in Ghica's Slot Games. The cost associated to a strategy is polynomially related to the normalization time of the interpreted proof, in the style of a complexity-theoretical full abstraction result.
<!--{{{-->
<div class='header' macro='gradient vert [[ColorPalette::PrimaryLight]] [[ColorPalette::PrimaryMid]]'>
<div class='headerShadow'>
<span class='siteTitle' refresh='content' tiddler='SiteTitle'></span>
<span class='siteSubtitle' refresh='content' tiddler='SiteSubtitle'></span>
</div>
<div class='headerForeground'>
<span class='siteTitle' refresh='content' tiddler='SiteTitle'></span>
<span class='siteSubtitle' refresh='content' tiddler='SiteSubtitle'></span>
</div>
</div>
<div id='mainMenu' refresh='content' tiddler='MainMenu'></div>
<div id='sidebar'>
<div id='sidebarOptions' refresh='content' tiddler='SideBarOptions'></div>
</div>
<div id='displayArea'>
<div id='messageArea'></div>
<div id='tiddlerDisplay'></div>
</div>
<!--}}}-->
First name / Name / Institution
Vincent ATASSI LIPN - Université Paris13
Patrick BAILLOT Université Paris 13 et CNRS
Amir ~BEN-AMRAM ~Tel-Aviv Academic College
Guillaume BONFANTE INRIA - LORIA
Pierre BOUDES LIPN CNRS Univ. Paris 13
Paolo COPPOLA University of Udine
Vittoria COZZA Università degli studi di Bari
Ugo DAL LAGO Università di Bologna
Norman DANNER Wesleyan University
Daniel DE CARVALHO LORIA
Arnaud DURAND Université Paris 7
Marco GABOARDI Università di Torino
Emmanuel HAINRY Loria, UHP
Miki HERMANN LIX, Ecole Polytechnique
Paulin JACOBÉ DE NAUROIS CNRS / Université Paris 13
Reinhard KAHLE Centria and DM, Univ. de Coimbra
Elham KASHEFI CNRS - Laboratoire d'Informatique de Grenoble
Lars KRISTIANSEN Dept. of Math., University of Oslo
Olivier LAURENT PPS
Harry MAIRSON Brandeis University
~Jean-Yves MARION LORIA INPL
Damiano MAZZA PPS - Université Paris 7
Richard MCKINLEY University of Bern
Virgile MOGBIL LIPN Univ. Paris13
~Jean-Yves MOYEN LIPN - CNRS - Univ. Paris 13
Isabel OITAVEM UNL and CMAF, Univ. de Lisboa
Romain PÉCHOUX LORIA
Mauro PICCOLO University of Turin - PPS
Simona RONCHI DELLA ROCCA Universita' di Torino
Luca ROVERSI Dipartimento di Informatica - Torino
James ROYER Syracuse University
Alexis SAURIN LIX - Ecole Polytechnique & INRIA
Stefan SCHIMANSKI LMU München
Ulrich SCHOEPP University of Munich
Olha SHKARAVSKA Radboud University Nijmegen
~François-Régis SINOT LSV ENS Cachan
Kazushige TERUI NII/LIPN
Pierre VALARCHER Université Paris 12
Marko VAN EEKELEN Radboud University Nijmegen
Jacqueline VAUZEILLES LIPN CNRS Univ. Paris 13
Luca VERCELLI Università di torino
!!!Implicit Computational Complexity
Implicit Computational Complexity (ICC) has emerged from various propositions to use logic and formal methods like types, rewriting systems, interpretations... to provide languages for complexity-bounded computation, in particular for polynomial time computing.
It aims at studying the computational complexity of programs without refering to a particular machine model and explicit bounds on time or memory, but instead by relying on programming or logical disciplines that imply complexity properties. Several approaches have been explored for that purpose, like restrictions on primitive recursion, lambda calculus, types, linear logic, rewriting systems .... They originally mostly came from the functional programming paradigm, but imperative programming is now also addressed. Two objectives of ICC are:
* on the one hand to find natural implicit logical characterizations of functions of various complexity classes,
* on the other hand to design criteria usable for the static verification of programs complexity. In particular the latter goal requires characterizations which are flexible enough to validate commonly used algorithms.
!!!Invited Speakers
* [[Simona Ronchi Della Rocca|http://www.di.unito.it/~ronchi/]], Università di Torino,
* [[Lars Kristiansen|http://www.iu.hio.no/~larskri/]], University of Oslo.
!!!Previous related meetings
* [[ICC Workshop|http://lipn.fr/~baillot/GEOCAL06/ICCworkshop.html]], Marseille, February 2006
* [[ICC and Logic meeting|http://lipn.fr/~baillot/workshopGEOCAL/complexite.html]], Villetaneuse, September 2004
!!!Organizers
* [[Pierre Boudes|http://www-lipn.univ-paris13.fr/~boudes/s/]], LIPN, Univ. Paris 13 - CNRS
* [[Paulin Jacobé de Naurois|http://www-lipn.univ-paris13.fr/~denaurois/]] (contact), LIPN, Univ. Paris 13 - CNRS
* [[Virgile Mogbil|http://www-lipn.univ-paris13.fr/~mogbil/]], LIPN, Univ. Paris 13 - CNRS
Online registration is now closed.
Lunch on the campus of Villetaneuse are included at no fees. If you have any trouble with the web form simply drop us an email.
Social event is programmed on monday evening at the [[//brasserie Flo//|http://www.flobrasseries.com/brasseries/index.asp?brasserie=5]] (7, cour des Petites Ecuries = entrée par le 63 rue du Fg Saint Denis, 75010 Paris, Métro : Château d’eau, Tel : 01 47 70 13 59).
Institution: Centria, UNL and DM, Universidade de Coimbra
[[Slides|slides/slides_Kahle_wicc08.pdf]]
Title: Recursion schemata for NC^k
Abstract: We give a recursion-theoretic characterization of the complexity classes NC^k. It uses no explicit bounds in the recursion and also no separation of variables is needed. This is joint work with G. Bonfante, J.-Y. Marion (both Nancy) and I. Oitavem (Lisbon).
Institution: University of Bern
Title: Soft Linear Set Theory
Abstract: The compatibility between light linear/affine logic and naive set theory is well known, and it has been shown (in detail) by Terui that the provably total functions of this system are precisely the polytime functions. In this talk we give some details of the analogous result for Lafont's Soft Linear Logic. The novelty of this system is the presence of a natural variable separation analogous to that of safe recursion that is crucial for establishing Polytime completeness.
Institution: LORIA Nancy
[[Slides|slides/slides_Pechoux_wicc08.pdf]]
Title: On the complexity of object oriented programs
Abstract: : A sup-interpretation is a tool which provides an upper bound on the size of a value computed by the function symbols of a program. Sup-interpretations have shown their interest to deal with the complexity of first order functional programs. For instance, they allow to characterize all the functions bitwise computable in Alogtime. This paper is an attempt to adapt the framework of sup-interpretations to a fragment of oriented-object programs, including loop and while constructs and non recursive methods with side effects. We give a criterion, called brotherly criterion, which uses to notion of sup-interpretation to ensure that each brotherly program computes objects whose size is polynomially bounded by the inputs sizes and we give some heuristics in order to compute the sup-interpretation of a given method.
<<search>><<closeAll>><<permaview>><<saveChanges>>
Institution: Università di Torino
[[Slides|slides/slides_Ronchi_wicc08.pdf]]
Title: Soft Linear Logic and Polynomial Complexity classes
Abstract: A recent research field in Theoretical Computer Science is the design of programming languages with bounded computational complexity. One of the more promising approaches to the design of programming languages with bounded complexity is based on the used of lambda-calculus as paradigmatic programming language, and on the design of type assignment systems for lambda-terms, where types guarantee, besides the functional correctness, also the desired complexity bound.
So the complexity can be checked statically at compilation time, in ML style. Here we will describe some results inspired to Lafonts Soft Linear Logic (SLL) which is a subsystem of second-order linear logic with restricted rules for exponentials, correct and complete for polynomial time computations. SLL has been the basis for the design of type assignment systems for lambda-calculus, characterizing the complexity classes PTIME, PSPACE and NP. PTIME is characterized by STA, a type assignments system where types are a proper subset of SLL formulae. The characterization consists in the fact that a term which can be typed in STA can be reduced to normal form by a number of beta-reductions polynomial in its lenght, and moreover all polynomial time functions can be computed by terms typable in this system. PSPACE is characterized by STAB, a type assignment system obtained from STA, by extending the set of types by a type B for booleans, and the lambda-calculus by two boolean constants and a conditional constructor. STAB assigns types to terms in such a way that the evaluation of programs (closed terms of type B) can be performed carefully in polynomial space. Moreover all polynomial space decision problems can be computed by terms typable in this system. The characterization of the complexity class NPTIME is made through the type assignment system STAP. Namely the lambda-calculus is extended by a nondeterministic choice operator +, and STAP is just STA plus a rule for dealing with this new term constructor.
<html><br></html>
February 11-12-13, 2008, Villetaneuse (Paris)
LIPN, Université Paris 13 & CNRS, supported by the ANR project [[NO-CoST|http://lipn.fr/nocost/rubrique.php3?id_rubrique=5]]
Workshop on Implicit Computational Complexity
Institution: LMU Munich
[[Slides|slides/slides_Schimanski_wicc08.pdf]]
Title: A Light Linear T
Abstract: Light Linear Logic and variants are extensionally complete for polynomial time. Some algorithms like unary polynomials and insertion sort can be expressed in a natural way, others require tricks to squeeze them into the shape of light linear iteration. The most basic example is the iteration of the successor applied to an unary number which is typed asymmetrical in the naive formulation. Another example is the split function of merge sort which is hard to write down with (D)LAL. We define a light linear variant of Goedel's T with ! and levels which can type these and other examples easily with a symmetric type without clever reformulation.
Institution: Università di Bologna
[[Slides|slides/slides_Dal_Lago_wicc08.pdf]]
Title: Quantum Implicit Computational Complexity
Abstract: We present a lambda calculus with classical control and quantum data characterizing quantum complexity classes such as EQP and BQP. The calculus is obtained by constraining Q (an already existing Turing-complete quantum lambda calculus) being inspired by Soft Linear Logic.
Institution: LMU Munich
[[Slides|slides/slides_Schoepp_wicc08.pdf]]
Title: Stratified Bounded Affine Logic for Logarithmic Space
Abstract: A number of complexity classes have been characterised by sub-systems of linear logic. This talk will be about Stratified Bounded Affine Logic (SBAL), a restricted version of linear logic that characterises the functions computable in LOGSPACE. SBAL is a restricted version of Bounded Linear Logic, in which not only the modality `!' but also the universal quantifier is bounded by a resource polynomial. Proofs of certain sequents in SBAL represent the functions computable logarithmic space. The translation of ~SBAL-proofs to ~LOGSPACE-functions is based on modelling computation by interaction dialogues in a version of the Geometry of Interaction. The purpose of this talk is to introduce SBAL, to outline how ~SBAL-proofs can be compiled to LOGSPACE programs and to discuss possibilities for simplification and extension.
<!--{{{-->
<div class='toolbar' macro='toolbar closeTiddler closeOthers +editTiddler'></div>
<div class='title' macro='view title'></div>
<div class='viewer' macro='view text wikified'></div>
<div class='tagClear'></div>
<!--}}}-->
Institution: Universita' di Bari
(Joint work with Salvatore Caporaso, Universita' di Bari)
[[Slides|slides/slides_Cozza_wicc08.pdf]]
Title : Feasible ICC C and its Harmonization with the Provable Hierarchy
Abstract.: Sometimes ICC is criticized for its limited role in real life programming. We introduce here a language FC (=Feasible C), which is obtained by means of a few restrictions to C. Its syntax only allows polytime programs; so feasibility is controlled at compile time. Many C programs can be transformed uniformly into FC programs, by simply prefixing some directives (pre-processing instructions). This has been checked on most examples and exercises contained in the celebrated textbook by Kernighan & Ritchie, and, in particular, to all recursion schemes they code. In practice, the mentioned restrictions allow a "static verification of programs complexity by a characterization which is flexible enough to validate commonly used algorithms" [this CFP]. In principle, we don't make much more than adaptating to C the classical distinction between safe variables and normal ones, and taking advantage of the pointer to string data type. A second goal of our research is a taxonomy collecting and connecting as many subrecursive classes as possible, in a unified taxonomy, defined by a few criteria. The existing subrecursive hierarchies are either slow to the point of needing $\epsilon_0$ to exhaust the elementary functions, or fast to the point of moving in a single step from linear time to all k-super-exp-time classes. And in both cases, they don't cope, by reasons we try to point-out, with the ICC philosophy. By progressive weakenings of our ICC restrictions to C we present here a hierarchy $C_\alpha$ that characterizes: dtime(n^k) at k, dtime(n_k) at $\omega+k$, the Grzegorczyk classes E_k at $\omega^k$ and the $\Sigma_k$-ind fragments of recursive arithmetics at $\omega_k$. This harmonizes the poly-time classes with the provable hierarchy.