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
Pulcini Gabriele
Abstract: We illustrate a combinatorial approach to geometry of 2-dim. manifolds based on //pq-permutations// (specific mathematical structures originate in theambit of topological studies on linear proofs). We show that pq-permutations allow to simplify Massey's algorithm for computing surfaces and provide a very useful framework inwhich to study processes of decomposition. Moreover, we propose are formulation of classification in a strictly combinatorial and operational way.
Les groupes de travail LAC (Logique, Algèbre et Calcul) et GEOCAL (Géométrie du calcul) du GDR Informatique Mathématique organisent leur réunion annelle 2008 en commun à l'Université Paris 13 (Campus de Villetaneuse) du 6 au 7 mars 2008.
Nous vous invitons dès à présent à regarder le programme et à vous inscrire à l'aide du menu de gauche (Inscription) et ce jusqu'au 24 Février 2008.
Les exposés se dérouleront dans l'amphithéatre Euler (Hall du batiment principal de l'institut Galilée, noté 2 sur le [[plan|http://lipn.fr/planfac/?lang=fr#campus]]). Les déjeuners pourront être pris au restaurant de l'université. Une liste d'hôtels est disponible.
!!!Thématiques
La problématique générale du groupe de travail [[GEOCAL|http://iml.univ-mrs.fr/~regnier/gdr-im/]] (//Géométrie du calcul//) est de trouver au sein de la logique et des mathématiques des outils permettant la modélisation abstraite des programmes. Un exemple spectaculaire du succès de cette approche est l'invention de la logique linéaire issue d'une part de l'isomorphisme de Curry - Howard établissant la correspondance entre les déductions formelles en logique intuitionniste et le lambda-calcul typé, et d'autre part de la modélisation du lambda-calcul par des espaces présentant des analogies fortes avec les espaces vectoriels.
Le groupe de travail [[LAC|http://www.pps.jussieu.fr/~kesner/gdr/lac.html]] (//Logique, Algèbre et Calcul//) a pour but de fédérer des chercheurs français travaillant sur les interactions entre les systèmes calculatoires dont la théorie est issue de l'algèbre, comme les systèmes de réécriture de premier ordre ou les automates d'arbres, et ceux dont la base provient plutôt d'un système logique (intuitionniste, classique, linéaire) comme le lambda-calcul ou les réseaux de preuve/interaction sans oublier les formalismes informatiques issus de la théorie des catégories. Notre but est d'une part, d'exploiter le transfert de techniques entre ces formalismes, et d'autre part, d'étudier la possibilité de faire coexister ces approches dans un cadre homogène qui intègrent plusieurs paradigmes. Les thèmes pourraient se regrouper en (i) fondements, (ii) techniques et (iii) applications et implémentations.
!!!Précédentes réunions
[[GEOCAL|http://iml.univ-mrs.fr/~regnier/gdr-im/]] et [[LAC|http://www.pps.jussieu.fr/~kesner/gdr/reunions.html]].
!!! Comité d'organisation
[[Patrick Baillot|http://www-lipn.univ-paris13.fr/~baillot/]] (LIPN), [[Micaela Mayero|http://www-lipn.univ-paris13.fr/~mayero]] (LIPN), [[Virgile Mogbil|http://www-lipn.univ-paris13.fr/~mogbil]] (LIPN).
Pour le thème des catégories pour l'informatique : [[Dominique Duval|http://ljk.imag.fr/membres/Dominique.Duval/]] et [[Francois Lamarche|http://www.loria.fr/~lamarche/]].
Bonjour à tous,
Les groupes de travail LAC (Logique, Algèbre et Calcul) et GEOCAL (Géométrie du calcul) du GDR Informatique Mathématique organisent leur réunion annelle 2008 en commun à l'Université Paris 13 (Campus de Villetaneuse) du 6 au 8 mars 2008.
Nous vous invitons dès à présent à vous inscrire et à proposer éventuellement un exposé, en vous rendant sur le site de la rencontre : http://lipn.fr/~mogbil/gdr-im08
Ces informations sont à communiquer jusqu'au 1er Février 2008 pour les propositions d'exposés et jusqu'au 24 Février 2008 pour les inscriptions.
Nous comptons commencer jeudi 6 mars matin, et terminer samedi 8 mars aux alentours de midi. Tout cela reste, bien sûr, fonction des demandes que nous recevrons. Notez qu'une demi-journée sera consacrée au thème des catégories pour l'informatique.
Les exposés se dérouleront dans l'amphithéatre Euler (batiment principal de l'institut Galilée, voir site).
Une liste d'hôtels sera indiquée sur le site. Les déjeuners pourront être pris au restaurant de l'université. N'hésitez pas à nous contacter si vous avez besoin d'un renseignement en précisant dans le sujet "[GEOCAL+LAC]".
A bientot,
Patrick Baillot, Micaela Mayero et Virgile Mogbil.
S'il y a dans votre laboratoire des gens qui pourraient être intéressés, n'hésitez pas à leur transmettre cette annonce.
Houtmann Clément
Abstract : We present a highly configurable deduction system for predicate logic called superdeduction modulo, resulting of the combination of deduction modulo and superdeduction which are two orthogonal presentations of predicate logic. It enables the user to make a distinct use of computational and reasoning axioms in a sound and complete manner. We show that by using permutations ofinference rules, any cut-free proof in deduction modulo can be transformed into a cut-free proof in superdeduction modulo and conversely. As a corollary we obtain that cut-elimination for deduction modulo (which is well-studied) is equivalent to cut-elimination for superdeduction modulo provided that some hypotheses on the synchrony of reasoning axioms areverified. Finally we propose a tableau method based on superdeduction modulo which is sound and complete provided that cut-elimination holds.
Pagani Michele
Abstract: I present a strict correspondence between cut-elimination, acyclicity and finiteness spaces in the framework of differential nets with promotion (DN for short). DN have been defined by Ehrhard&Regnier as an extension of the multiplicative exponential linear logic, introducing the semantical constructions defined by Ehrhard in his finiteness spaces.
Consider the orthogonal (P)° of a net P with conclusion C as the set of all nets R with a conclusion notC s.t. the cut between C and notC is weak normalizable. Let P be a cut-free net with conclusion C, my results show that the following conditions are equivalent:
1. P is interpreted as a finitary relation in the finiteness space associated with C
2. P is visible acyclic (a geometric condition more general than the usual Danos&Regnier's correctness criterion)
3. (P)° contains all visible acyclic nets with conclusion notC
These equivalences provide a generalization of the ones in the main theorems of the theory of linear logic proof-nets, namely: Retoré's theorem (1 -> 2), semantic soundness theorem (2 -> 1), weak normalization theorem (2 -> 3), and Bechét's theorem (3 -> 2). Above all, it discloses a deep unity in DN among normalization, visible acyclicity and finiteness spaces, which was present (even if never actually remarked) only in the multiplicative fragment of linear logic.
Background: #fff
Foreground: #000
PrimaryPale: #840
PrimaryLight: #f80
PrimaryMid: #840
PrimaryDark: #000
SecondaryPale: #ffc
SecondaryLight: #fe8
SecondaryMid: #db4
SecondaryDark: #841
TertiaryPale: #eee
TertiaryLight: #ccc
TertiaryMid: #999
TertiaryDark: #666
Error: #f88
Terui Kazushige
Abstract: We present a computationally adapted version of Girard's ludics, aiming at giving a foundational framework for the computability and complexity theory. We introduce a handy syntax for designsthat simplifies Curien's concrete syntax and extends it with explicit cuts and identities. We also consider design generators that allow for finite representation of some infinite designs. A normalization procedure in the style of Krivine's abstract machine works on generators directly, giving rise to an effective means of normalization.
Our extended system enjoys the analytical theorems of ludics in a suitably modified form. In addition, we prove a general form of full completeness with respect to coinductively defined behaviours and infinitary proofs.
Finally, an analysis is made on those designs representing data objects.We show that any set of finite data forms a behaviour, and then discuss acceptance of languages via normalization.
''Proposition d'exposé'' : jusqu'au 1er Février 2008
''Notification'' : 11 Février 2008
''Inscription'' : jusqu'au 24 Février 2008
''Réunion'' : 6-7 Mars 2008
Herbelin Hugo
Résumé : Aucune des interprétations calculatoires du calcul des séquents sous la forme d'un calcul exhibant une dualité appel par nom / appel par valeur n'a jusque là capturé à la fois l'ensemble des preuves normales du calcul des séquents tout en validant les règles de type éta. On montre comment l'introduction d'un opérateur de "paresse" permet d'atteindre cet objectif. On introduit aussi une notion de connecteur purement calculatoire qui capture tout autant les types algébriques à la ML et les connecteurs synthétiques de Girard que les notions d'abstraction et d'application.
~Paul-André Melliès
Résumé : Dans cet exposé, j'expliquerai comment la sémantique des jeux peut être interprétée comme un diagramme de corde, offrant le reflet topologique d'une situation catégorique particulière. De cette analyse découle une logique du tenseur et de la négation -- appelée logique tensorielle. Je décrirai comment les preuves de cette logique peuvent être présentées par des stratégies génératrices 3-dimensionnelles dans une bicatégorie monoidale -- de la même manière que les noeuds topologiques sont présentes par des générateurs 2-dimensionnels dans des catégories monoidales. Pour finir, j'esquisserai comment cette étude menée, après les travaux de Day et Street, a une définition 2-dimensionnelle et relachée d'algèbre de Frobenius.
Kaczmarek Matthieu
Résumé : Nous proposons une construction efficace pour la détectionmorphologique de programmes malicieux. Cette détection considère les graphesde flot de contrôle (GFC) comme des signatures. Nous présentons commentréaliser de manière efficace une telle détection. D'une part nous employonsla théorie des automates d'arbre afin de représenter la base de donnée de GFC malicieux. L'existence d'automates d'arbre minimaux garantie unereprésentation compacte et efficace. D'autre part, nous présentons commenttraiter de manière générique les mutations grâce à un moteur de réécriturede graphe. Finallement, nous présentons des résultats expérimentaux afin devalider empiriquement cette stratégie de détection.Travail de thèse réalisé sous la direction de ~Jean-Yves Marion et Guillaume Bonfante
Yves Lafont
(en collaboration avec François Métayer et Krzysztof Worytkiewicz).
Résumé : Le programme de Minneapolis (Lafont & Métayer) propose un cadre homotopique pour la théorie de la réécriture à base de catégories de dimension supérieure (omega-catégories strictes). L'idée naïve est qu'une cellule de dimension n+1 représente une homotopie entre cellules de dimension n. En fait, on a besoin d'une notion plus générale de "n-cylindre", décrite explicitement par Métayer, et dont la définition a été simplifiée récemment. Ces cylindres forment eux-mêmes une omega-catégorie. Nous parlerons aussi de la "réversibilité", une version faible de l'inversibilité qui se définit par coinduction. Ces notions ne demandent pas de connaissances particulières en théorie de l'homotopie (ou de l'homologie). Elles sont utilisées dans deux articles récents :
*Yves Lafont & François Métayer, Polygraphic resolutions and homology of monoids (soumis à publication)
*Yves Lafont, François Métayer & Krzysztof Worytkiewicz, A folk model structure on omega-cat (en préparation)
Envoyez nous par email les informations suivantes jusqu'au 1er Février 2008 pour les propositions d'exposés et jusqu'au 24 Février 2008 pour les inscriptions. Le programme est accessible dans le menu de gauche.
/%
Si vous souhaitez faire une proposition d'exposé sur le thème des catégories, merci de mettre en copie les personnes suivantes :
Dominique.Duval {_at_} imag.fr , Francois.Lamarche {_at_} loria.fr
%/
//Email: // Micaela.Mayero {_at_} lipn.fr
//Sujet: // [GEOCAL+LAC 2008] Inscription
----------------------------------------------------------------------
Nom :
Prénom :
Institution :
Adresse complète :
Tel :
Fax :
E-mail :
GT du GDR : GEOCAL - LAC
Repas de midi : aucun - jeudi - vendredi
* Je souhaite participer en tant qu'auditeur. /%* Je souhaite participer en tant qu'orateur, je propose un exposé dont le titre et le résumé sont :%/
* Je sollicite un soutien financier à hauteur de :
----------------------------------------------------------------------
Catégories pour l'informatique
|bgcolor:#04b;color:#fff; 9h30 - 10h00 || //Accueil// |
|bgcolor:#04b;color:#fff; 10h00 - 10h45 ||bgcolor:#abf; [[Paul-André Melliès]] De la sémantique des jeux comme diagramme de cordes |
|bgcolor:#04b;color:#fff; 10h45 - 11h15 || //Pause Café// |
|bgcolor:#04b;color:#fff; 11h15 - 12h00 ||bgcolor:#abf; [[Tom Hirschowitz]] Une théorie des théories des jeux |
|bgcolor:#04b;color:#fff; 12h00 - 12h30 ||bgcolor:#abf; [[Aurélien Pardon]] Une approche essentiellement algébrique et modulaire de la syntaxe avec lieurs |
|bgcolor:#04b;color:#fff; 12h30 - 13h00 ||bgcolor:#abf; [[Simon Perdrix]] Sémantique catégorique du transfert d'état quantique |
|bgcolor:#04b;color:#fff; 13h00 - 14h30 || //Déjeuner// |
|bgcolor:#04b;color:#fff; 14h30 - 15h15 ||bgcolor:#abf; [[Sergei Soloviev]] La théorie des preuves dans l'étude des catégories non-libres |
|bgcolor:#04b;color:#fff; 15h15 - 16h00 ||bgcolor:#abf; [[Olivier Laurent]] Sur les modèles catégoriques de la logique linéaire élémentaire |
|bgcolor:#04b;color:#fff; 16h00 - 16h30 || //Pause café// |
|bgcolor:#04b;color:#fff; 16h30 - 17h15 ||bgcolor:#abf; [[Yves Lafont]] Homotopie en dimension supérieure |
|bgcolor:#04b;color:#fff; 17h15 - 17h45 ||bgcolor:#abf; [[Gabriele Pulcini]] A combinatorial approach to geometry of 2-dimensional manifolds |
|bgcolor:#04b;color:#fff; 17h45 - 18h15 || Discussion |
Burel Guillaume
Résumé : La superdéduction est un formalisme proche de la déduction modulo, qui permet d'enrichir un système de déduction du premier ordre (comme le calcul des séquences et la déduction naturelle) avec de nouvelles règles d'inférence qui sont calculées automatiquement à partir de la présentation d'une théorie. Nous donnons un encodage naturel de tout système de type pure(PTS) fonctionnel en superdéduction, en définissant une théorie du premier ordre appropriée. Nous prouvons que la traduction est correcte et conservatrice, ce qui montre une correspondance entre les jugements de typage valides dans le PTS et les séquences prouvables dans le système de superdéduction correspondant.
Nous introduisons également le calcul des séquences superdéductif intuitionniste, qui était auparavant défini uniquement en logique classique.Nous montrons son équivalence avec la déduction naturelle superdéductive.Ceci implique que la superdéduction peut être facilement utilisée comme cadre logique. Ces résultats tendent vers une meilleure compréhension de l'implémentation et de la recherche de preuve pour les PTS, ainsi que vers plus de coopération entre les assistants à la démonstration.
Sergei Soloviev
Résumé : Les méthodes de preuve assez traditionnelles (permutation des règles, analyse des preuves séquentielles) sont utilisées pour étudier la commutativité des diagrammes dans les catégories non-libres. Le principal fait utilisé est que l'égalité dans les catégories non-libres est « miroitée » par une relation d'équivalence sur les dérivations qui contient l'équivalence « minimale » de la catégorie libre. Le cas central : les catégories symétriques monoïdales fermées (par exemple, les modules au-dessus d'un anneau commutatif avec unité). Le résultat central : l'existence de l'axiomatisation canonique d'une équivalence « non-libre » par un ensemble de « paires critiques ». On discute des propriétés des équivalences non-libres et on donne quelques exemples.
(L'exposé est en partie basé sur le travail effectué avec Laurent Mehats)
La réunion a lieu sur le campus de Villetaneuse de l'université Paris 13, au nord proche de Paris (environ 25 minutes depuis la Gare du Nord). Les exposés se dérouleront dans l'amphithéatre Euler (Hall du bâtiment principal de l'institut Galilée, noté 2 sur le [[plan|http://lipn.fr/planfac/?lang=fr#campus]]).
!!!Depuis Paris -- [[Details ici|http://lipn.fr/planfac/?lang=fr]]
*Train de Gare du Nord jusqu'à la gare d'Epinay - Villetaneuse (en Gare du Nord, suivre l'une des directions Ermont - Eaubonne, Luzarches, Persan - Beaumont ou Valmondois en vérifiant, sur le quai de départ, que le train s'arrête en gare d'Epinay - Villetaneuse)
*En Gare d'Epinay - Villetaneuse, sortie côté Villetaneuse puis bus jusqu'à l'arrêt Université Paris 13 : bus 156 (direction Gare de St - Denis) ou bus 354 (direction Pierrefitte - Stains) ou bus 356 (direction St - Denis Université).
!!Hotels
Voici une liste d'hotel situés dans Paris intramuros, relativement près de la gare du Nord, où sont les trains desservant notre université. Aucun autre critère n'est pris en compte dans cette sélection, si ce n'est qu'ils ont un site au moins informatif.
Pour ceux qui préfèrent regarder par eux-même, nous vous recommandons le moteur de recherche suivant : [[trouver un hôtel|http://en.parisinfo.com/paris-hotels/hotels-1/]].
Nous vous conseillons de choisir un hôtel près de la gare du Nord ou près du quartier Latin qui a une liaison rapide avec la gare du Nord).
---------------------------------------------------------------------------
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
(D'après http://www.liafa.jussieu.fr/~mairesse/Sda2/)
Pour poster :
* Tout abonné d'une des listes de diffusion de gdr-im peut poster sur n'importe laquelle des autres listes. Il faut noter cependant que l'envoyeur du message ne le recevra pas s'il n'est pas abonné à la liste.
* Les listes sont configurées par défaut avec réponse à l'envoyeur (et non pas à toute la liste).
Les listes qui nous concernent sont :
gt-lac@gdr-im.fr : Logique Algèbre et Calcul
gt-geocal@gdr-im.fr : Géométrie du Calcul
[[Accueil]]
[[Dates importantes]]
[[Programme]]
[[Participants]]
[[Lieu et accès]]
<html>
<a href="http://lipn.fr" target="_blank">
<img src="http://www-lipn.univ-paris13.fr/image/LIPN_logo.jpg" width="100" alt="LIPN"></a>
</html>
Ruyer Frédéric
Résumé: Nous présentons une classe de modèles du lambda-calcul et de la logique du second ordre. Les modèles sont basés sur des treillis et interprètent la réduction, ainsi que la relation de réalisabilité, à l'aide de la relation d'ordre. Nous tenterons de dégager les liens avec les algèbres de Heyting et les modèles à base de cpo du lambda-calcul.
Vaux Lionel
Abstract: We extend ~Ehrhard-Regnier's differential linear logic to a classical logic setting, by means of a polarization à la Laurent. We define cut elimination in this system following a denotational semantics in a pure (i.e. untyped) model in the category of sets and relations. Then we show how to interpret the new rules of this logical system as syntactical constructions on the stacks (aka environments) of Herbelin's lambda-bar-mu-calculus, the dynamics of which is derived from cut elimination. Last, we study how structural equalities induced by both operational and denotational semantics allow to break beta-reduction into multiplicative and exponential reductions: this provide a convenient framework to introduce differentiation inside lambda-bar-mu-calculus.
<!--{{{-->
<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>
<!--}}}-->
Abbes Samy (PPS, Université Paris 7)
Agon Carlos (Ircam)
Allali Lisa (INRIA)
Andreatta Moreno (Ircam/CNRS)
Aravantinos Vincent (Laboratoire d'Informatique de Grenoble)
Atassi Vincent (LIPN, Université Paris 13)
Baillot Patrick (LIPN/CNRS,Université Paris 13)
Boudol Gérard (INRIA Sophia Antipolis, Équipe Mimosa)
Brauner Paul (LORIA)
Burel Guillaume (~Nancy-Université - LORIA)
Crolard Tristan (LACL, Université Paris 12)
Duchesne Etienne (Institut de Mathématiques de Luminy)
Duval Dominique (Université Joseph Fourier Grenoble)
Dumas ~Jean-Guillaume (Laboratoire Jean Kuntzmann)
de Falco Marc (Institut de Mathématiques de Luminy)
Fouqueré Christophe (LIPN, Université Paris 13)
Fousse Laurent (Laboratoire Jean Kuntzmann)
Fumex Clément (LAMA, Université de Savoie)
Gimenez Stéphane (PPS, Université Paris 7)
Guenot Nicolat (LIX)
Hatat Florian (LAMA, Université de Savoie)
Herbelin Hugo (INRIA)
Hirschkoff Daniel (ENS Lyon)
Hirschowitz Michel (CEA)
Hirschowitz Tom (CNRS - LAMA, Université de Savoie)
Hyvernat Pierre (LAMA, Université de Savoie)
Houtmann Clément (Université Henri Poincaré Nancy 1)
Jacobé de Naurois Paulin (LIPN, CNRS/Université Paris 13)
Kaczmarek Matthieu (Loria - INPL)
Kesner Delia (PPS, Université Paris 7)
Lafont Yves (Institut de Mathématiques de Luminy)
Lamarche François (INRIA)
Laurent Olivier (PPS, CNRS - Université Paris 7)
Lengrand Stéphane (CNRS - Laboratoire d'Informatique de l'Ecole Polytechnique)
Malbos Philippe (Institut Camille Jordan, Université Lyon 1)
Mayero Micaela (LIPN, Université Paris 13)
Méhats Laurent (INRIA)
Métayer François (PPS, Université Paris 7)
Mimram Samuel (PPS, Université Paris 7)
Mogbil Virgile (LIPN, Université Paris 13)
Pagani Michele (PPS, Université Paris 7)
Perdrix Simon (Oxford University Computing Laboratory)
Piccolo Mauro (Università di Torino)
Polonowski Emmanuel (LACL, Université Paris 12)
Prouté Alain (Université Paris 7)
Pulcini Gabriele (LIPN, Université Paris 13)
Régnier Laurent (Institut de Mathématiques de Luminy)
Sinot ~François-Régis (ENS Cachan)
Soloviev Sergei (IRIT)
Tabareau Nicolas (PPS, Université Paris 7)
Tasson Christine (PPS, Université Paris 7)
Terui Kazushige (NII (Tokyo) et LIPN)
Vautier Alexandre (IRISA)
Vaux Lionel (Institut de Mathématiques de Luminy)
Zimmermann Stéphane (INRIA)
Duchesne Etienne
Résumé : On montre qu'on peut associer à certains points fixes de la GdI d'une preuve (à ceux complets en un certain sens) un ensemble de points de sa sémantique relationnelle. Plus précisément on leur associe des formules prouvables de la logique linéaire indexée, qui sont des expériences calculant des familles de points de la sémantique d'une preuve.
<html>
<a href="javascript:void(0)" onclick="story.closeAllTiddlers();story.displayTiddlers(null,['Programme','De la sémantique des jeux comme diagramme de cordes','Une théorie des théories des jeux','Sémantique catégorique du transfert d état quantique','La théorie des preuves dans l étude des catégories non-libres','Sur les modèles catégoriques de la logique linéaire élémentaire','Homotopie en dimension supérieure','A combinatorial approach to geometry of 2-dimensional manifolds','De l utilité d un opérateur de paresse pour interpréter calculatoirement le calcul des séquents','Une preuve sémantique de normalisation pour le système T','Modèles pour le calcul et la logique','Computational Ludics','Points fixes de la GdI et logique linéaire indexée','Between interaction and semantics: visible acyclic nets','Détection morphologique de programme malicieux','On differential linear logic and polarization','Axiom directed Focusing','La superdéduction comme cadre logique'])">Affichage de tous les résumés (en bas de la page)</a>, cliquer sur le titre de l'exposé pour avoir le résumé correspondant, et <a href="javascript:void(0)" onclick="story.closeAllTiddlers();story.displayTiddlers(null,['Programme'])">ici pour enlever tous les résumés.</a></html>
!!Jeudi 6 mars 2008, //Catégories pour l'Informatique//
*//09h45 - 10h00 Accueil//
*10h00 - 10h45 ''~Paul-André Melliès'' : [[De la sémantique des jeux comme diagramme de cordes]]
*//10h45 - 11h15 Pause Café//
*11h15 - 12h00 ''Tom Hirschowitz'' (en collaboration avec André et Michel Hirschowitz) : [[Une théorie des théories des jeux]] - [[Slides|slides/hirschowitz-geocal-lac-2008.pdf]]
*12h00 - 12h30 ''Aurélien Pardon'' : [[Une approche essentiellement algébrique et modulaire de la syntaxe avec lieurs]] - [[Slides|slides/pardon-geocal-lac-2008.pdf]]
*12h30 - 13h00 ''Simon Perdrix'' (en collaboration avec Bob Coecke et Eric Paquette) : [[Sémantique catégorique du transfert d état quantique]] - [[Slides|slides/perdrix-geocal-lac-2008.pdf]]
*//13h00 - 14h30 Déjeuner//
*14h30 - 15h15 ''Sergei Soloviev'' : [[La théorie des preuves dans l étude des catégories non-libres]] - [[Slides|slides/soloviev-geocal-lac-2008.pdf]]
*15h15 - 16h00 ''Olivier Laurent'' : [[Sur les modèles catégoriques de la logique linéaire élémentaire]] - [[Slides|slides/laurent-geocal-lac-2008.pdf]]
*//16h00 - 16h30 Pause café//
*16h30 - 17h15 ''Yves Lafont'' (en collaboration avec François Métayer et Krzysztof Worytkiewicz) : [[Homotopie en dimension supérieure]] - [[Slides|slides/lafont-geocal-lac-2008.pdf]]
*17h15 - 17h45 ''Gabriele Pulcini'' : [[A combinatorial approach to geometry of 2-dimensional manifolds]]
*17h45 - 18h15 Discussion
!!Vendredi 7 mars 2008
*09h30 - 10h00 ''Hugo Herbelin'' : [[De l utilité d un opérateur de paresse pour interpréter calculatoirement le calcul des séquents]]
*10h00 - 10h30 ''Paul Brauner'' (en collaboration avec Lisa Allali) : [[Une preuve sémantique de normalisation pour le système T]]
*10h30 - 11h00 ''Frédéric Ruyer'' : [[Modèles pour le calcul et la logique]] - [[Slides|slides/ruyer-geocal-lac-2008.pdf]]
*//11h00 - 11h30 Pause café//
*11h30 - 12h00 ''Kazushige Terui'' : [[Computational Ludics]]
*12h00 - 12h30 ''Etienne Duchesne'' : [[Points fixes de la GdI et logique linéaire indexée]] - [[Slides|slides/duchesne-geocal-lac-2008.pdf]]
*12h30 - 13h00 ''Michele Pagani'' : [[Between interaction and semantics: visible acyclic nets]] - [[Slides|slides/pagani-geocal-lac-2008.pdf]]
*//13h00 - 14h30 Déjeuner//
*14h30 - 15h00 ''Gérard Boudol'' : [[Réalisabilité pour un langage impératif (et concurrent) d'ordre supérieur]] - [[Slides|slides/boudol-geocal-lac-2008.pdf]]
*15h00 - 15h30 ''Matthieu Kaczmarek'' : [[Détection morphologique de programme malicieux]] - [[Slides|slides/kaczmarek-geocal-lac-2008.pdf]]
*15h30 - 16h00 ''Lionel Vaux'' : [[On differential linear logic and polarization]]
*//16h00 - 16h30 Pause café//
*16h30 - 17h00 ''Clément Houtmann'' : [[Axiom directed Focusing]] - [[Slides|slides/houtmann-geocal-lac-2008.pdf]]
*17h00 - 17h30 ''Guillaume Burel'' : [[La superdéduction comme cadre logique]] - [[Slides|slides/burel-geocal-lac-2008.pdf]]
Des ordinateurs sont à votre disposition en salles G207 et G215 (depuis l'amphi. Euler : au dernier étage puis à gauche). Voici le compte linux pour vous connecter :
Login/password : gdr-im / 37=40Moins3
Ces salles, usuellement en accès libre, vous sont réservées. Malheureusement elles ne permettent pas d'utiliser votre ordinateur personnel. Les ordinateurs sont en dual boot, aussi vous pouvez redémarrer les machines sous Windows (Ctr+Alt+Supp, comme indiqué ) puis passer sous Linux au moment du redémarrage (utiliser les flèches haut-bas).
<<search>><<closeAll>><<permaview>><<saveChanges>>
<<tabs txtMainTab "Timeline" "Timeline" TabTimeline "All" "All tiddlers" TabAll "Tags" "All tags" TabTags "More" "More lists" TabMore>>
6-7 Mars 2008, Villetaneuse (Paris)
LIPN, Université Paris 13 & CNRS
Réunion des groupes de travail
[[GEOCAL|http://iml.univ-mrs.fr/~regnier/gdr-im/]] (Géométrie du calcul) et
[[LAC|http://www.pps.jussieu.fr/~kesner/gdr/lac.html]] (Logique, Algèbre et Calcul) du
[[GDR IM|http://www.gdr-im.fr/]] (Informatique Mathématique)
http://lipn.fr/~mogbil/gdr-im08
Olivier Laurent
Résumé : Nous proposons une definition de modele categorique de la logique lineaire elementaire (ELL) dans le style des modeles de Seely de la logique lineaire (LL).
Les connecteurs additifs pour ELL etant definis par une condition non locale sur les reseaux (cf. [~DanosJoinet2003]), l'interpretation des preuves dans nos modeles necessite de generaliser le cadre habituel utilise en logique categorique : connecteur -> foncteur.
Le connecteur ! est ici decompose a l'aide d'un pre-connecteur # qui n'est pas interprete par un foncteur mais par toute une famille de foncteurs (engendree par l'identite, tenseur et avec).
En application, on obtient une condition simple permettant de determiner si un sous-modele d'un modele de LL est un modele de ELL avec connecteurs additifs.
[~DanosJoinet2003] Vincent Danos and ~Jean-Baptiste Joinet: Linear logic and elementary time. Information and Computation 183(1):123-137 (2003)
Simon Perdrix
Résumé : Abramsky et Coecke [~AC04] ont proposé une axiomatisation catégorique de la mécanique quantique en termes de catégories fortement compactes closes (aussi appelées catégories dagger compactes closes). Cette axiomatisation leur a permis de mettre en évidence les structures fondamentales de protocoles quantiques comme la téléportation. Je vais présenter un langage graphique pour les catégories fortement compactes closes permettant de donner une sémantique catégorique à de nouveaux protocoles quantiques, notamment le transfert d'état [P05] . Ce protocole a été introduit pour diminuer les ressources du calcul quantique par mesures. La mise en évidence des structures du transfert d'état constitue donc un pas supplémentaire vers la découverte des structures fondamentales du calcul quantique.
*[~AC04] S. Abramsky and B. Coecke, A categorical semantics of quantum protocols. Proceedings of ~LiCS'04, pp.415–425, IEEE Computer Science Press, 2004.
*[P05] S. Perdrix. State transfer instead of teleportation in measurement-based quantum computation. International Journal of Quantum Information, 3(1):219-223, 2005.
Travail en collaboration avec Bob Coecke et Eric Paquette.
Type the text for 'TiddlyWiki'
Brauner Paul
(Travail conjoint de Lisa Allali et Paul Brauner)
Résumé : Les méthodes sémantiques sont utilisées depuis longtemps pour prouver l'élimination des coupures. Ce n'est que récemment qu'elles ont été étendues aux preuves de forte normalisation. Cependant, elles ne s'appliquent pas aux systèmes avec récurseurs comme le système T de Gödel. Nous montrons comment la logique avec fold/unfold de Prawitz fournit un pont entre la superconsistence de l'arithmétique et la forte normalisation du système T. Nous verrons ensuite comment ce résultat s'étend a une famille de types inductifs.
Tom Hirshowitz
(En collaboration avec André et Michel Hirschowitz.)
Résumé : La sémantique des jeux a fait ses preuves comme source de modèles pleinement abstraits pour langages de programmation ou théories de la démonstration. De tels modèles apparaissent comme catégories de jeux et stratégies, mais on en compte de nombreuses variantes, qu'on ne sait pas bien relier entre elles. D'où la question: qu'est-ce qu'une catégorie de jeux et stratégies ?
On donne une définition catégorique générale de jeu, en décrivant la catégorie de stratégies associée. On définit ensuite une construction catégorique générant un jeu à partir de données plus élémentaires. On montre comment les jeux de Hyland et Ong avec switching entrent dans ce cadre.
|bgcolor:#04b;color:#fff; 9h30 - 10h00 ||bgcolor:#abf; [[Hugo Herbelin]] De l'utilité d'un opérateur de paresse pour interpréter calculatoirement le calcul des séquents |
|bgcolor:#04b;color:#fff;10h00 - 10h30 ||bgcolor:#abf; [[Paul Brauner]] Une preuve sémantique de normalisation pour le système T |
|bgcolor:#04b;color:#fff; 10h30 - 11h00 ||bgcolor:#abf; [[Frédéric Ruyer]] Modèles pour le calcul et la logique |
|bgcolor:#04b;color:#fff; 11h00 - 11h30 || //Pause café// |
|bgcolor:#04b;color:#fff; 11h30 - 12h00 ||bgcolor:#abf; [[Kazushige Terui]] Computational Ludics |
|bgcolor:#04b;color:#fff; 12h00 - 12h30 ||bgcolor:#abf; [[Etienne Duchesne]] Points fixes de la GdI et logique linéaire indexée |
|bgcolor:#04b;color:#fff; 12h30 - 13h00 ||bgcolor:#abf; [[Michele Pagani]] Between interaction and semantics: visible acyclic nets |
|bgcolor:#04b;color:#fff; 13h00 - 14h30 || //Déjeuner// |
|bgcolor:#04b;color:#fff; 14h30 - 15h00 ||bgcolor:#abf; [[Gérard Boudol]] Réalisabilité pour un langage impératif (et concurrent) d'ordre supérieur |
|bgcolor:#04b;color:#fff; 15h30 - 16h00 ||bgcolor:#abf; [[Matthieu Kaczmarek]] Détection morphologique de programme malicieux |
|bgcolor:#04b;color:#fff; 16h00 - 16h30 ||bgcolor:#abf; [[Lionel Vaux]] On differential linear logic and polarization |
|bgcolor:#04b;color:#fff; 16h30 - 17h00 || //Pause café// |
|bgcolor:#04b;color:#fff; 17h00 - 17h30 ||bgcolor:#abf; [[Clément Houtmann]] Axiom directed Focusing |
|bgcolor:#04b;color:#fff; 17h30 - 18h00 ||bgcolor:#abf; [[Guillaume Burel]] La superdéduction comme cadre logique |
<!--{{{-->
<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>
<!--}}}-->