WFRF:(Weber Tjark)
Sökning: WFRF:(Weber Tjark) > Psi-Calculi in Isab...
LIBRIS Formathandbok (Information om MARC21)
| Fältnamn | Indikatorer | Metadata |
|---|---|---|
| 000 | 02766naa a2200373 4500 | |
| 001 | oai:DiVA.org:uu-275571 | |
| 003 | SwePub | |
| 008 | 160204s2016 | |||||||||||000 ||eng| | |
| 024 | 7 | a https://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-2755712 URI |
| 024 | 7 | a https://doi.org/10.1007/s10817-015-9336-22 DOI |
| 040 | a (SwePub)uu | |
| 041 | a engb eng | |
| 042 | 9 SwePub | |
| 072 | 7 | a ref2 swepub-contenttype |
| 072 | 7 | a art2 swepub-publicationtype |
| 100 | 1 | a Bengtson, Jesperu IT Univ Copenhagen, Copenhagen, Denmark.4 aut |
| 245 | 1 0 | a Psi-Calculi in Isabelle |
| 264 | c 2015-08-19 | |
| 264 | 1 | b Springer Science and Business Media LLC,c 2016 |
| 338 | a print2 rdacarrier | |
| 520 | a This paper presents a mechanisation of psi-calculi, a parametric framework for modelling various dialects of process calculi including (but not limited to) the pi-calculus, the applied pi-calculus, and the spi calculus. psi-calculi are significantly more expressive, yet their semantics is as simple in structure as the semantics of the original pi-calculus. Proofs of meta-theoretic properties for psi-calculi are more involved, however, not least because psi-calculi (unlike simpler calculi) utilise binders that bind multiple names at once. The mechanisation is carried out in the Nominal Isabelle framework, an interactive proof assistant designed to facilitate formal reasoning about calculi with binders. Our main contributions are twofold. First, we have developed techniques that allow efficient reasoning about calculi that bind multiple names in Nominal Isabelle. Second, we have adopted these techniques to mechanise substantial results from the meta-theory of psi-calculi, including congruence properties of bisimilarity and the laws of structural congruence. To our knowledge, this is the most extensive formalisation of process calculi mechanised in a proof assistant to date. | |
| 650 | 7 | a NATURVETENSKAPx Data- och informationsvetenskapx Datavetenskap0 (SwePub)102012 hsv//swe |
| 650 | 7 | a NATURAL SCIENCESx Computer and Information Sciencesx Computer Sciences0 (SwePub)102012 hsv//eng |
| 653 | a Psi-calculi | |
| 653 | a Process calculi | |
| 653 | a Proof assistants | |
| 653 | a Nominal logic | |
| 653 | a Mechanisation | |
| 700 | 1 | a Parrow, Joachimu Uppsala universitet,Datalogi4 aut0 (Swepub:uu)jpa23056 |
| 700 | 1 | a Weber, Tjarku Uppsala universitet,Datalogi4 aut0 (Swepub:uu)tjawe125 |
| 710 | 2 | a IT Univ Copenhagen, Copenhagen, Denmark.b Datalogi4 org |
| 773 | 0 | t Journal of automated reasoningd : Springer Science and Business Media LLCg 56:1, s. 1-47q 56:1<1-47x 0168-7433x 1573-0670 |
| 856 | 4 8 | u https://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-275571 |
| 856 | 4 8 | u https://doi.org/10.1007/s10817-015-9336-2 |
Hitta via bibliotek
- Journal of automated reasoning (Sök värdpublikationen i LIBRIS)
Till lärosätets databas
Hitta mer i SwePub
- Av författaren/redakt...
- Bengtson, Jesper
- Parrow, Joachim
- Weber, Tjark
- Om ämnet
-
- NATURVETENSKAP
- NATURVETENSKAP
- och Data och informa ...
- och Datavetenskap
- Artiklar i publikationen
- Journal of autom ...
- Av lärosätet
- Uppsala universitet
Sök utanför SwePub
- Sök vidare i:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - Nationella bibliotekssystem
- LIBRIS.kb.se
