Unifying Theories in Isabelle/HOL
Identifieur interne : 001264 ( Main/Corpus ); précédent : 001263; suivant : 001265Unifying Theories in Isabelle/HOL
Auteurs : Abderrahmane Feliachi ; Marie-Claude Gaudel ; Burkhart WolffSource :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2010.
English descriptors
- KwdEn :
- Circus , CSP, Isabelle/HOL, Theorem Proving, UTP.
Abstract
Abstract: In this paper, we present various extensions of Isabelle/HOL by theories that are essential for several formal methods. First, we explain how we have developed an Isabelle/HOL theory for a part of the Unifying Theories of Programming (UTP). It contains the theories of alphabetized relations and designs. Then we explain how we have encoded first the theory of reactive processes and then the UTP theory for CSP. Our work takes advantage of the rich existing logical core of HOL. Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and Circus . The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation.
Url:
DOI: 10.1007/978-3-642-16690-7_9
Links to Exploration step
ISTEX:04FFF401263AA42FBAB822701FA466DB30761B37Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Unifying Theories in Isabelle/HOL</title><author><name sortKey="Feliachi, Abderrahmane" sort="Feliachi, Abderrahmane" uniqKey="Feliachi A" first="Abderrahmane" last="Feliachi">Abderrahmane Feliachi</name><affiliation><mods:affiliation>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</mods:affiliation></affiliation><affiliation><mods:affiliation>CNRS, F-91405, Orsay, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Abderrahmane.Feliachi@lri.fr</mods:affiliation></affiliation></author><author><name sortKey="Gaudel, Marie Claude" sort="Gaudel, Marie Claude" uniqKey="Gaudel M" first="Marie-Claude" last="Gaudel">Marie-Claude Gaudel</name><affiliation><mods:affiliation>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</mods:affiliation></affiliation><affiliation><mods:affiliation>CNRS, F-91405, Orsay, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Marie-Claude.Gaudel@lri.fr</mods:affiliation></affiliation></author><author><name sortKey="Wolff, Burkhart" sort="Wolff, Burkhart" uniqKey="Wolff B" first="Burkhart" last="Wolff">Burkhart Wolff</name><affiliation><mods:affiliation>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</mods:affiliation></affiliation><affiliation><mods:affiliation>CNRS, F-91405, Orsay, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Burkhart.Wolff@lri.fr</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:04FFF401263AA42FBAB822701FA466DB30761B37</idno><date when="2010" year="2010">2010</date><idno type="doi">10.1007/978-3-642-16690-7_9</idno><idno type="url">https://api.istex.fr/document/04FFF401263AA42FBAB822701FA466DB30761B37/fulltext/pdf</idno><idno type="wicri:Area/Main/Corpus">001264</idno><idno type="wicri:explorRef" wicri:stream="Main" wicri:step="Corpus" wicri:corpus="ISTEX">001264</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Unifying Theories in Isabelle/HOL</title><author><name sortKey="Feliachi, Abderrahmane" sort="Feliachi, Abderrahmane" uniqKey="Feliachi A" first="Abderrahmane" last="Feliachi">Abderrahmane Feliachi</name><affiliation><mods:affiliation>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</mods:affiliation></affiliation><affiliation><mods:affiliation>CNRS, F-91405, Orsay, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Abderrahmane.Feliachi@lri.fr</mods:affiliation></affiliation></author><author><name sortKey="Gaudel, Marie Claude" sort="Gaudel, Marie Claude" uniqKey="Gaudel M" first="Marie-Claude" last="Gaudel">Marie-Claude Gaudel</name><affiliation><mods:affiliation>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</mods:affiliation></affiliation><affiliation><mods:affiliation>CNRS, F-91405, Orsay, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Marie-Claude.Gaudel@lri.fr</mods:affiliation></affiliation></author><author><name sortKey="Wolff, Burkhart" sort="Wolff, Burkhart" uniqKey="Wolff B" first="Burkhart" last="Wolff">Burkhart Wolff</name><affiliation><mods:affiliation>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</mods:affiliation></affiliation><affiliation><mods:affiliation>CNRS, F-91405, Orsay, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Burkhart.Wolff@lri.fr</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2010</date></imprint><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series><idno type="istex">04FFF401263AA42FBAB822701FA466DB30761B37</idno><idno type="DOI">10.1007/978-3-642-16690-7_9</idno><idno type="ChapterID">Chap9</idno><idno type="ChapterID">9</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term> Circus </term><term>CSP</term><term>Isabelle/HOL</term><term>Theorem Proving</term><term>UTP</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In this paper, we present various extensions of Isabelle/HOL by theories that are essential for several formal methods. First, we explain how we have developed an Isabelle/HOL theory for a part of the Unifying Theories of Programming (UTP). It contains the theories of alphabetized relations and designs. Then we explain how we have encoded first the theory of reactive processes and then the UTP theory for CSP. Our work takes advantage of the rich existing logical core of HOL. Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and Circus . The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation.</div></front></TEI><istex><corpusName>springer</corpusName><author><json:item><name>Abderrahmane Feliachi</name><affiliations><json:string>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</json:string><json:string>CNRS, F-91405, Orsay, France</json:string><json:string>E-mail: Abderrahmane.Feliachi@lri.fr</json:string></affiliations></json:item><json:item><name>Marie-Claude Gaudel</name><affiliations><json:string>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</json:string><json:string>CNRS, F-91405, Orsay, France</json:string><json:string>E-mail: Marie-Claude.Gaudel@lri.fr</json:string></affiliations></json:item><json:item><name>Burkhart Wolff</name><affiliations><json:string>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</json:string><json:string>CNRS, F-91405, Orsay, France</json:string><json:string>E-mail: Burkhart.Wolff@lri.fr</json:string></affiliations></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>UTP</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Theorem Proving</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Isabelle/HOL</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>CSP</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Circus</value></json:item></subject><language><json:string>eng</json:string></language><abstract>Abstract: In this paper, we present various extensions of Isabelle/HOL by theories that are essential for several formal methods. First, we explain how we have developed an Isabelle/HOL theory for a part of the Unifying Theories of Programming (UTP). It contains the theories of alphabetized relations and designs. Then we explain how we have encoded first the theory of reactive processes and then the UTP theory for CSP. Our work takes advantage of the rich existing logical core of HOL. Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and Circus . The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation.</abstract><qualityIndicators><score>8.384</score><pdfVersion>1.6</pdfVersion><pdfPageSize>429.725 x 659.895 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractCharCount>948</abstractCharCount><pdfWordCount>6821</pdfWordCount><pdfCharCount>36554</pdfCharCount><pdfPageCount>19</pdfPageCount><abstractWordCount>157 </abstractWordCount></qualityIndicators><title>Unifying Theories in Isabelle/HOL</title><genre><json:string>Original Paper</json:string></genre><serie><editor><json:item><name>David Hutchison</name><affiliations><json:string>Lancaster University, Lancaster, UK</json:string></affiliations></json:item><json:item><name>Takeo Kanade</name><affiliations><json:string>Carnegie Mellon University, Pittsburgh, PA, USA</json:string></affiliations></json:item><json:item><name>Josef Kittler</name><affiliations><json:string>University of Surrey, Guildford, UK</json:string></affiliations></json:item><json:item><name>Jon M. Kleinberg</name><affiliations><json:string>Cornell University, Ithaca, NY, USA</json:string></affiliations></json:item><json:item><name>Friedemann Mattern</name><affiliations><json:string>ETH Zurich, Zurich, Switzerland</json:string></affiliations></json:item><json:item><name>John C. Mitchell</name><affiliations><json:string>Stanford University, Stanford, CA, USA</json:string></affiliations></json:item><json:item><name>Moni Naor</name><affiliations><json:string>Weizmann Institute of Science, Rehovot, Israel</json:string></affiliations></json:item><json:item><name>Oscar Nierstrasz</name><affiliations><json:string>University of Bern, Bern, Switzerland</json:string></affiliations></json:item><json:item><name>C. Pandu Rangan</name><affiliations><json:string>Indian Institute of Technology, Madras, India</json:string></affiliations></json:item><json:item><name>Bernhard Steffen</name><affiliations><json:string>University of Dortmund, Dortmund, Germany</json:string></affiliations></json:item><json:item><name>Madhu Sudan</name><affiliations><json:string>Massachusetts Institute of Technology, MA, USA</json:string></affiliations></json:item><json:item><name>Demetri Terzopoulos</name><affiliations><json:string>University of California, Los Angeles, CA, USA</json:string></affiliations></json:item><json:item><name>Doug Tygar</name><affiliations><json:string>University of California, Berkeley, CA, USA</json:string></affiliations></json:item><json:item><name>Moshe Y. Vardi</name><affiliations><json:string>Rice University, Houston, TX, USA</json:string></affiliations></json:item><json:item><name>Gerhard Weikum</name><affiliations><json:string>Max-Planck Institute of Computer Science, Saarbrücken, Germany</json:string></affiliations></json:item></editor><issn><json:string>0302-9743</json:string></issn><genre></genre><language><json:string>unknown</json:string></language><title>Lecture Notes in Computer Science</title><copyrightDate>2010</copyrightDate></serie><host><volume>6445</volume><editor><json:item><name>Shengchao Qin</name><affiliations><json:string>School of Computing, University of Teesside, Borough Road, TS1 3BA, Middlesbrough, UK</json:string><json:string>E-mail: s.qin@tees.ac.uk</json:string></affiliations></json:item></editor><pages><last>206</last><first>188</first></pages><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Logics and Meanings of Programs</value></json:item><json:item><value>Software Engineering</value></json:item><json:item><value>Programming Languages, Compilers, Interpreters</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item><json:item><value>Programming Techniques</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item></subject><isbn><json:string>978-3-642-16689-1</json:string></isbn><genre><json:string>Proceedings</json:string><json:string>eBook</json:string></genre><language><json:string>unknown</json:string></language><title>Unifying Theories of Programming</title><copyrightDate>2010</copyrightDate><doi><json:string>10.1007/978-3-642-16690-7</json:string></doi></host><copyrightDate>2010</copyrightDate><doi><json:string>10.1007/978-3-642-16690-7_9</json:string></doi><id>04FFF401263AA42FBAB822701FA466DB30761B37</id><fulltext><json:item><original>true</original><mimetype>application/pdf</mimetype><extension>pdf</extension><uri>https://api.istex.fr/document/04FFF401263AA42FBAB822701FA466DB30761B37/fulltext/pdf</uri></json:item><json:item><original>false</original><mimetype>application/zip</mimetype><extension>zip</extension><uri>https://api.istex.fr/document/04FFF401263AA42FBAB822701FA466DB30761B37/fulltext/zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/04FFF401263AA42FBAB822701FA466DB30761B37/fulltext/tei"><teiHeader type="text"><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Unifying Theories in Isabelle/HOL</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><date>2010</date></publicationStmt><notesStmt><note>This work was partially supported by the Digiteo Foundation.</note></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Unifying Theories in Isabelle/HOL</title><author><persName><forename type="first">Abderrahmane </forename><surname>Feliachi</surname></persName><email>Abderrahmane.Feliachi@lri.fr</email><affiliation>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</affiliation><affiliation>CNRS, F-91405, Orsay, France</affiliation></author><author><persName><forename type="first">Marie-Claude </forename><surname>Gaudel</surname></persName><email>Marie-Claude.Gaudel@lri.fr</email><affiliation>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</affiliation><affiliation>CNRS, F-91405, Orsay, France</affiliation></author><author><persName><forename type="first">Burkhart </forename><surname>Wolff</surname></persName><email>Burkhart.Wolff@lri.fr</email><affiliation>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</affiliation><affiliation>CNRS, F-91405, Orsay, France</affiliation></author></analytic><monogr><title level="m">Unifying Theories of Programming</title><title level="m" type="sub">Third International Symposium, UTP 2010, Shanghai, China, November 15-16, 2010. Proceedings</title><idno type="pISBN">978-3-642-16689-1</idno><idno type="eISBN">978-3-642-16690-7</idno><idno type="DOI">10.1007/978-3-642-16690-7</idno><idno type="BookID">978-3-642-16690-7</idno><idno type="BookTitleID">214761</idno><idno type="BookSequenceNumber">6445</idno><idno type="BookVolumeNumber">6445</idno><idno type="BookChapterCount">15</idno><editor><persName><forename type="first">Shengchao </forename><surname>Qin</surname></persName><email>s.qin@tees.ac.uk</email><affiliation>School of Computing, University of Teesside, Borough Road, TS1 3BA, Middlesbrough, UK</affiliation></editor><imprint><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><date>2010</date><biblScope unit="vol">6445</biblScope><biblScope unit="page" from="188">188</biblScope><biblScope unit="page" to="206">206</biblScope></imprint></monogr><series><title level="s">Lecture Notes in Computer Science</title><editor><persName><forename type="first">David </forename><surname>Hutchison</surname></persName><affiliation>Lancaster University, Lancaster, UK</affiliation></editor><editor><persName><forename type="first">Takeo </forename><surname>Kanade</surname></persName><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation></editor><editor><persName><forename type="first">Josef </forename><surname>Kittler</surname></persName><affiliation>University of Surrey, Guildford, UK</affiliation></editor><editor><persName><forename type="first">Jon M. </forename><surname>Kleinberg</surname></persName><affiliation>Cornell University, Ithaca, NY, USA</affiliation></editor><editor><persName><forename type="first">Friedemann </forename><surname>Mattern</surname></persName><affiliation>ETH Zurich, Zurich, Switzerland</affiliation></editor><editor><persName><forename type="first">John C. </forename><surname>Mitchell</surname></persName><affiliation>Stanford University, Stanford, CA, USA</affiliation></editor><editor><persName><forename type="first">Moni </forename><surname>Naor</surname></persName><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation></editor><editor><persName><forename type="first">Oscar </forename><surname>Nierstrasz</surname></persName><affiliation>University of Bern, Bern, Switzerland</affiliation></editor><editor><persName><forename type="first">C. </forename><surname>Pandu Rangan</surname></persName><affiliation>Indian Institute of Technology, Madras, India</affiliation></editor><editor><persName><forename type="first">Bernhard </forename><surname>Steffen</surname></persName><affiliation>University of Dortmund, Dortmund, Germany</affiliation></editor><editor><persName><forename type="first">Madhu </forename><surname>Sudan</surname></persName><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation></editor><editor><persName><forename type="first">Demetri </forename><surname>Terzopoulos</surname></persName><affiliation>University of California, Los Angeles, CA, USA</affiliation></editor><editor><persName><forename type="first">Doug </forename><surname>Tygar</surname></persName><affiliation>University of California, Berkeley, CA, USA</affiliation></editor><editor><persName><forename type="first">Moshe Y. </forename><surname>Vardi</surname></persName><affiliation>Rice University, Houston, TX, USA</affiliation></editor><editor><persName><forename type="first">Gerhard </forename><surname>Weikum</surname></persName><affiliation>Max-Planck Institute of Computer Science, Saarbrücken, Germany</affiliation></editor><biblScope><date>2010</date></biblScope><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="seriesId">558</idno></series><idno type="istex">04FFF401263AA42FBAB822701FA466DB30761B37</idno><idno type="DOI">10.1007/978-3-642-16690-7_9</idno><idno type="ChapterID">Chap9</idno><idno type="ChapterID">9</idno></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2010</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: In this paper, we present various extensions of Isabelle/HOL by theories that are essential for several formal methods. First, we explain how we have developed an Isabelle/HOL theory for a part of the Unifying Theories of Programming (UTP). It contains the theories of alphabetized relations and designs. Then we explain how we have encoded first the theory of reactive processes and then the UTP theory for CSP. Our work takes advantage of the rich existing logical core of HOL. Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and Circus . The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation.</p></abstract><textClass xml:lang="en"><keywords scheme="keyword"><list><head>Keywords</head><item><term>UTP</term></item><item><term>Theorem Proving</term></item><item><term>Isabelle/HOL</term></item><item><term>CSP</term></item><item><term> Circus </term></item></list></keywords></textClass><textClass><keywords scheme="Book Subject Collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass><keywords scheme="Book Subject Group"><list><label>I</label><item><term>Computer Science</term></item><label>I1603X</label><item><term>Logics and Meanings of Programs</term></item><label>I14029</label><item><term>Software Engineering</term></item><label>I14037</label><item><term>Programming Languages, Compilers, Interpreters</term></item><label>I16048</label><item><term>Mathematical Logic and Formal Languages</term></item><label>I14010</label><item><term>Programming Techniques</term></item><label>I21017</label><item><term>Artificial Intelligence (incl. Robotics)</term></item></list></keywords></textClass></profileDesc></teiHeader></istex:fulltextTEI><json:item><original>false</original><mimetype>text/plain</mimetype><extension>txt</extension><uri>https://api.istex.fr/document/04FFF401263AA42FBAB822701FA466DB30761B37/fulltext/txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Springer, Publisher found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>David</GivenName><FamilyName>Hutchison</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Takeo</GivenName><FamilyName>Kanade</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Josef</GivenName><FamilyName>Kittler</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jon</GivenName><GivenName>M.</GivenName><FamilyName>Kleinberg</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Friedemann</GivenName><FamilyName>Mattern</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>John</GivenName><GivenName>C.</GivenName><FamilyName>Mitchell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff7"><EditorName DisplayOrder="Western"><GivenName>Moni</GivenName><FamilyName>Naor</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff8"><EditorName DisplayOrder="Western"><GivenName>Oscar</GivenName><FamilyName>Nierstrasz</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff9"><EditorName DisplayOrder="Western"><GivenName>C.</GivenName><FamilyName>Pandu Rangan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff10"><EditorName DisplayOrder="Western"><GivenName>Bernhard</GivenName><FamilyName>Steffen</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff11"><EditorName DisplayOrder="Western"><GivenName>Madhu</GivenName><FamilyName>Sudan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff12"><EditorName DisplayOrder="Western"><GivenName>Demetri</GivenName><FamilyName>Terzopoulos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff13"><EditorName DisplayOrder="Western"><GivenName>Doug</GivenName><FamilyName>Tygar</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff14"><EditorName DisplayOrder="Western"><GivenName>Moshe</GivenName><GivenName>Y.</GivenName><FamilyName>Vardi</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff15"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Weikum</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Lancaster University</OrgName><OrgAddress><City>Lancaster</City><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>University of Surrey</OrgName><OrgAddress><City>Guildford</City><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff4"><OrgName>Cornell University</OrgName><OrgAddress><City>Ithaca</City><State>NY</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgName>ETH Zurich</OrgName><OrgAddress><City>Zurich</City><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff6"><OrgName>Stanford University</OrgName><OrgAddress><City>Stanford</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgName>Weizmann Institute of Science</OrgName><OrgAddress><City>Rehovot</City><Country>Israel</Country></OrgAddress></Affiliation><Affiliation ID="Aff8"><OrgName>University of Bern</OrgName><OrgAddress><City>Bern</City><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff9"><OrgName>Indian Institute of Technology</OrgName><OrgAddress><City>Madras</City><Country>India</Country></OrgAddress></Affiliation><Affiliation ID="Aff10"><OrgName>University of Dortmund</OrgName><OrgAddress><City>Dortmund</City><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff11"><OrgName>Massachusetts Institute of Technology</OrgName><OrgAddress><State>MA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff12"><OrgName>University of California</OrgName><OrgAddress><City>Los Angeles</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff13"><OrgName>University of California</OrgName><OrgAddress><City>Berkeley</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff14"><OrgName>Rice University</OrgName><OrgAddress><City>Houston</City><State>TX</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff15"><OrgName>Max-Planck Institute of Computer Science</OrgName><OrgAddress><City>Saarbrücken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingDepth="2" NumberingStyle="ContentOnly" OutputMedium="All" TocLevels="0"><BookID>978-3-642-16690-7</BookID><BookTitle>Unifying Theories of Programming</BookTitle><BookSubTitle>Third International Symposium, UTP 2010, Shanghai, China, November 15-16, 2010. Proceedings</BookSubTitle><BookVolumeNumber>6445</BookVolumeNumber><BookSequenceNumber>6445</BookSequenceNumber><BookDOI>10.1007/978-3-642-16690-7</BookDOI><BookTitleID>214761</BookTitleID><BookPrintISBN>978-3-642-16689-1</BookPrintISBN><BookElectronicISBN>978-3-642-16690-7</BookElectronicISBN><BookChapterCount>15</BookChapterCount><BookCopyright><CopyrightHolderName>Springer Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2010</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I1603X" Priority="1" Type="Secondary">Logics and Meanings of Programs</BookSubject><BookSubject Code="I14029" Priority="2" Type="Secondary">Software Engineering</BookSubject><BookSubject Code="I14037" Priority="3" Type="Secondary">Programming Languages, Compilers, Interpreters</BookSubject><BookSubject Code="I16048" Priority="4" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><BookSubject Code="I14010" Priority="5" Type="Secondary">Programming Techniques</BookSubject><BookSubject Code="I21017" Priority="6" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff16"><EditorName DisplayOrder="Western"><GivenName>Shengchao</GivenName><FamilyName>Qin</FamilyName></EditorName><Contact><Email>s.qin@tees.ac.uk</Email></Contact></Editor><Affiliation ID="Aff16"><OrgDivision>School of Computing</OrgDivision><OrgName>University of Teesside</OrgName><OrgAddress><Street>Borough Road</Street><Postcode>TS1 3BA</Postcode><City>Middlesbrough</City><Country>UK</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Chapter ID="Chap9" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>9</ChapterID><ChapterDOI>10.1007/978-3-642-16690-7_9</ChapterDOI><ChapterSequenceNumber>9</ChapterSequenceNumber><ChapterTitle Language="En">Unifying Theories in Isabelle/HOL</ChapterTitle><ChapterFirstPage>188</ChapterFirstPage><ChapterLastPage>206</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2010</CopyrightYear></ChapterCopyright><ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><BookID>978-3-642-16690-7</BookID><BookTitle>Unifying Theories of Programming</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff17 Aff18"><AuthorName DisplayOrder="Western"><GivenName>Abderrahmane</GivenName><FamilyName>Feliachi</FamilyName></AuthorName><Contact><Email>Abderrahmane.Feliachi@lri.fr</Email></Contact></Author><Author AffiliationIDS="Aff17 Aff18"><AuthorName DisplayOrder="Western"><GivenName>Marie-Claude</GivenName><FamilyName>Gaudel</FamilyName></AuthorName><Contact><Email>Marie-Claude.Gaudel@lri.fr</Email></Contact></Author><Author AffiliationIDS="Aff17 Aff18"><AuthorName DisplayOrder="Western"><GivenName>Burkhart</GivenName><FamilyName>Wolff</FamilyName></AuthorName><Contact><Email>Burkhart.Wolff@lri.fr</Email></Contact></Author><Affiliation ID="Aff17"><OrgDivision>Laboratoire LRI, UMR8623</OrgDivision><OrgName>Univ Paris-Sud</OrgName><OrgAddress><City>Orsay</City><Postcode>F-91405</Postcode><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff18"><OrgName>CNRS</OrgName><OrgAddress><City>Orsay</City><Postcode>F-91405</Postcode><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>In this paper, we present various extensions of Isabelle/HOL by theories that are essential for several formal methods. First, we explain how we have developed an Isabelle/HOL theory for a part of the Unifying Theories of Programming (UTP). It contains the theories of alphabetized relations and designs. Then we explain how we have encoded first the theory of reactive processes and then the UTP theory for CSP. Our work takes advantage of the rich existing logical core of HOL.</Para><Para>Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and <Emphasis FontCategory="SansSerif" Type="Italic">Circus</Emphasis> . The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation.</Para></Abstract><KeywordGroup Language="En"><Heading>Keywords</Heading><Keyword>UTP</Keyword><Keyword>Theorem Proving</Keyword><Keyword>Isabelle/HOL</Keyword><Keyword>CSP</Keyword><Keyword><Emphasis FontCategory="SansSerif" Type="Italic">Circus</Emphasis></Keyword></KeywordGroup><ArticleNote Type="Misc"><SimplePara>This work was partially supported by the Digiteo Foundation.</SimplePara></ArticleNote></ChapterHeader><NoBody></NoBody></Chapter></Book></Series></Publisher></istex:document></istex:metadataXml><!--Version 0.11 générée le 11-8-2015--><mods version="3.6"><titleInfo lang="en"><title>Unifying Theories in Isabelle/HOL</title></titleInfo><titleInfo type="alternative" contentType="CDATA" lang="en"><title>Unifying Theories in Isabelle/HOL</title></titleInfo><name type="personal"><namePart type="given">Abderrahmane</namePart><namePart type="family">Feliachi</namePart><affiliation>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</affiliation><affiliation>CNRS, F-91405, Orsay, France</affiliation><affiliation>E-mail: Abderrahmane.Feliachi@lri.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Marie-Claude</namePart><namePart type="family">Gaudel</namePart><affiliation>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</affiliation><affiliation>CNRS, F-91405, Orsay, France</affiliation><affiliation>E-mail: Marie-Claude.Gaudel@lri.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Burkhart</namePart><namePart type="family">Wolff</namePart><affiliation>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay, France</affiliation><affiliation>CNRS, F-91405, Orsay, France</affiliation><affiliation>E-mail: Burkhart.Wolff@lri.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre>Original Paper</genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><copyrightDate encoding="w3cdtf">2010</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><physicalDescription><internetMediaType>text/html</internetMediaType></physicalDescription><abstract lang="en">Abstract: In this paper, we present various extensions of Isabelle/HOL by theories that are essential for several formal methods. First, we explain how we have developed an Isabelle/HOL theory for a part of the Unifying Theories of Programming (UTP). It contains the theories of alphabetized relations and designs. Then we explain how we have encoded first the theory of reactive processes and then the UTP theory for CSP. Our work takes advantage of the rich existing logical core of HOL. Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and Circus . The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation.</abstract><note>This work was partially supported by the Digiteo Foundation.</note><subject lang="en"><genre>Keywords</genre><topic>UTP</topic><topic>Theorem Proving</topic><topic>Isabelle/HOL</topic><topic>CSP</topic><topic> Circus </topic></subject><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">David</namePart><namePart type="family">Hutchison</namePart><affiliation>Lancaster University, Lancaster, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Takeo</namePart><namePart type="family">Kanade</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Josef</namePart><namePart type="family">Kittler</namePart><affiliation>University of Surrey, Guildford, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jon M.</namePart><namePart type="family">Kleinberg</namePart><affiliation>Cornell University, Ithaca, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Friedemann</namePart><namePart type="family">Mattern</namePart><affiliation>ETH Zurich, Zurich, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">John C.</namePart><namePart type="family">Mitchell</namePart><affiliation>Stanford University, Stanford, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moni</namePart><namePart type="family">Naor</namePart><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Oscar</namePart><namePart type="family">Nierstrasz</namePart><affiliation>University of Bern, Bern, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">C.</namePart><namePart type="family">Pandu Rangan</namePart><affiliation>Indian Institute of Technology, Madras, India</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Steffen</namePart><affiliation>University of Dortmund, Dortmund, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Madhu</namePart><namePart type="family">Sudan</namePart><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Demetri</namePart><namePart type="family">Terzopoulos</namePart><affiliation>University of California, Los Angeles, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Doug</namePart><namePart type="family">Tygar</namePart><affiliation>University of California, Berkeley, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moshe Y.</namePart><namePart type="family">Vardi</namePart><affiliation>Rice University, Houston, TX, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Weikum</namePart><affiliation>Max-Planck Institute of Computer Science, Saarbrücken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><copyrightDate encoding="w3cdtf">2010</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer Berlin Heidelberg, 2010</recordOrigin></recordInfo></relatedItem><relatedItem type="host"><titleInfo><title>Unifying Theories of Programming</title><subTitle>Third International Symposium, UTP 2010, Shanghai, China, November 15-16, 2010. Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Shengchao</namePart><namePart type="family">Qin</namePart><affiliation>School of Computing, University of Teesside, Borough Road, TS1 3BA, Middlesbrough, UK</affiliation><affiliation>E-mail: s.qin@tees.ac.uk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre>Proceedings</genre><genre>eBook</genre><originInfo><copyrightDate encoding="w3cdtf">2010</copyrightDate><issuance>monographic</issuance></originInfo><subject><genre>Book Subject Collection</genre><topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic></subject><subject><genre>Book Subject Group</genre><topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic><topic authority="SpringerSubjectCodes" authorityURI="I14029">Software Engineering</topic><topic authority="SpringerSubjectCodes" authorityURI="I14037">Programming Languages, Compilers, Interpreters</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic><topic authority="SpringerSubjectCodes" authorityURI="I14010">Programming Techniques</topic><topic authority="SpringerSubjectCodes" authorityURI="I21017">Artificial Intelligence (incl. Robotics)</topic></subject><identifier type="DOI">10.1007/978-3-642-16690-7</identifier><identifier type="ISBN">978-3-642-16689-1</identifier><identifier type="eISBN">978-3-642-16690-7</identifier><identifier type="BookTitleID">214761</identifier><identifier type="BookID">978-3-642-16690-7</identifier><identifier type="BookChapterCount">15</identifier><identifier type="BookVolumeNumber">6445</identifier><identifier type="BookSequenceNumber">6445</identifier><part><date>2010</date><detail type="volume"><number>6445</number><caption>vol.</caption></detail><extent unit="pages"><start>188</start><end>206</end></extent></part><recordInfo><recordOrigin>Springer Berlin Heidelberg, 2010</recordOrigin></recordInfo></relatedItem><identifier type="istex">04FFF401263AA42FBAB822701FA466DB30761B37</identifier><identifier type="DOI">10.1007/978-3-642-16690-7_9</identifier><identifier type="ChapterID">Chap9</identifier><identifier type="ChapterID">9</identifier><accessCondition type="use and reproduction" contentType="MetadataGrant">OpenAccess</accessCondition><accessCondition type="use and reproduction" contentType="AbstractGrant">OpenAccess</accessCondition><accessCondition type="use and reproduction" contentType="BodyPDFGrant">Restricted</accessCondition><accessCondition type="use and reproduction" contentType="BodyHTMLGrant">Restricted</accessCondition><accessCondition type="use and reproduction" contentType="BibliographyGrant">Restricted</accessCondition><accessCondition type="use and reproduction" contentType="ESMGrant">Restricted</accessCondition><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2010</recordOrigin></recordInfo></mods></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Wicri/explor/CircusV2/Data/Main/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001264 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Corpus/biblio.hfd -nk 001264 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Wicri
|area= CircusV2
|flux= Main
|étape= Corpus
|type= RBID
|clé= ISTEX:04FFF401263AA42FBAB822701FA466DB30761B37
|texte= Unifying Theories in Isabelle/HOL
}}
| This area was generated with Dilib version V0.6.31. |  |