59 Search Results for "Schmidt-Schauß, Manfred"

Volume

OASIcs, Volume 46

2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

WPTE 2015, July 2, 2015, Warsaw, Poland

Editors: Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, and Manfred Schmidt-Schauß

Volume

OASIcs, Volume 40

First International Workshop on Rewriting Techniques for Program Transformations and Evaluation

WPTE 2014, July 13, 2014, Vienna, Austria

Editors: Manfred Schmidt-Schauß, Masahiko Sakai, David Sabel, and Yuki Chiba

Volume

LIPIcs, Volume 10

22nd International Conference on Rewriting Techniques and Applications (RTA'11)

RTA 2011, May 30 to June 1, 2011, Novi Sad, Serbia

Editors: Manfred Schmidt-Schauss

Document
DOI: 10.4230/LIPIcs.FSCD.2022.7
Nominal Anti-Unification with Atom-Variables

Authors: Manfred Schmidt-Schauß and Daniele Nantes-Sobrinho

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Anti-unification is the task of generalizing a set of expressions in the most specific way. It was extended to the nominal framework by Baumgarter, Kutsia, Levy and Villaret, who defined an algorithm solving the nominal anti-unification problem, which runs in polynomial time. Unfortunately, when an infinite set of atoms are allowed in generalizations, a minimal complete set of solutions in nominal anti-unification does not exist, in general. In this paper, we present a more general approach to nominal anti-unification that uses atom-variables instead of explicit atoms, and two variants of freshness constraints: NL_A-constraints (with atom-variables), and Eqr-constraints based on Equivalence relations on atom-variables. The idea of atom-variables is that different atom-variables may be instantiated with identical or different atoms. Albeit simple, this freedom in the formulation increases its application potential: we provide an algorithm that is finitary for the NL_A-freshness constraints, and for Eqr-freshness constraints it computes a unique least general generalization. There is a price to pay in the general case: checking freshness constraints and other related logical questions will require exponential time. The setting of Baumgartner et al. is improved by the atom-only case, which runs in polynomial time and computes a unique least general generalization.
Cite as

Manfred Schmidt-Schauß and Daniele Nantes-Sobrinho. Nominal Anti-Unification with Atom-Variables. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:LIPIcs.FSCD.2022.7,
  author =	{Schmidt-Schau{\ss}, Manfred and Nantes-Sobrinho, Daniele},
  title =	{{Nominal Anti-Unification with Atom-Variables}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{7:1--7:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.7},
  URN =		{urn:nbn:de:0030-drops-162885},
  doi =		{10.4230/LIPIcs.FSCD.2022.7},
  annote =	{Keywords: Generalization, anti-unification, nominal algorithms, higher-order deduction}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.28
Nominal Unification with Atom and Context Variables

Authors: Manfred Schmidt-Schauß and David Sabel

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
Automated deduction in higher-order program calculi, where properties of transformation rules are demanded, or confluence or other equational properties are requested, can often be done by syntactically computing overlaps (critical pairs) of reduction rules and transformation rules. Since higher-order calculi have alpha-equivalence as fundamental equivalence, the reasoning procedure must deal with it. We define ASD1-unification problems, which are higher-order equational unification problems employing variables for atoms, expressions and contexts, with additional distinct-variable constraints, and which have to be solved w.r.t. alpha-equivalence. Our proposal is to extend nominal unification to solve these unification problems. We succeeded in constructing the nominal unification algorithm NomUnifyASD. We show that NomUnifyASD is sound and complete for this problem class, and outputs a set of unifiers with constraints in nondeterministic polynomial time if the final constraints are satisfiable. We also show that solvability of the output constraints can be decided in NEXPTIME, and for a fixed number of context-variables in NP time. For terms without context-variables and atom-variables, NomUnifyASD runs in polynomial time, is unitary, and extends the classical problem by permitting distinct-variable constraints.
Cite as

Manfred Schmidt-Schauß and David Sabel. Nominal Unification with Atom and Context Variables. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:LIPIcs.FSCD.2018.28,
  author =	{Schmidt-Schau{\ss}, Manfred and Sabel, David},
  title =	{{Nominal Unification with Atom and Context Variables}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{28:1--28:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.28},
  URN =		{urn:nbn:de:0030-drops-91983},
  doi =		{10.4230/LIPIcs.FSCD.2018.28},
  annote =	{Keywords: automated deduction, nominal unification, lambda calculus, functional programming}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.405
Two-Restricted One Context Unification is in Polynomial Time

Authors: Adrià Gascón, Manfred Schmidt-Schauß, and Ashish Tiwari

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
One Context Unification (1CU) extends first-order unification by introducing a single context variable. This problem was recently shown to be in NP, but it is not known to be solvable in polynomial time. We show that the case of 1CU where the context variable occurs at most twice in the input (1CU2r) is solvable in polynomial time. Moreover, a polynomial representation of all solutions can also be computed in polynomial time. The 1CU2r problem is important as it is used as a subroutine in polynomial time algorithms for several more-general classes of 1CU problem. Our algorithm can be seen as an extension of the usual rules of first-order unification and can be used to solve related problems in polynomial time, such as first-order unification of two terms that tolerates one clash. All our results assume that the input terms are represented as Directed Acyclic Graphs.
Cite as

Adrià Gascón, Manfred Schmidt-Schauß, and Ashish Tiwari. Two-Restricted One Context Unification is in Polynomial Time. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 405-422, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gascon_et_al:LIPIcs.CSL.2015.405,
  author =	{Gasc\'{o}n, Adri\`{a} and Schmidt-Schau{\ss}, Manfred and Tiwari, Ashish},
  title =	{{Two-Restricted One Context Unification is in Polynomial Time}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{405--422},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.405},
  URN =		{urn:nbn:de:0030-drops-54289},
  doi =		{10.4230/LIPIcs.CSL.2015.405},
  annote =	{Keywords: context unification, first-order unification, deduction, type checking}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.WPTE.2015
OASIcs, Volume 46, WPTE'15, Complete Volume

Authors: Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, and Manfred Schmidt-Schauß

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
OASIcs, Volume 46, WPTE'15, Complete Volume
Cite as

2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Proceedings{chiba_et_al:OASIcs.WPTE.2015,
  title =	{{OASIcs, Volume 46, WPTE'15, Complete Volume}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015},
  URN =		{urn:nbn:de:0030-drops-52644},
  doi =		{10.4230/OASIcs.WPTE.2015},
  annote =	{Keywords: Conference proceedings, Concurrent Programming, Formal Definitions and Theory, Specifying and Verifying and Reasoning about Programs, Semantics of Programming Languages, Mathematical Logic, Grammars and Other Rewriting Systems, Deduction and Theorem Proving}
}
Document
Front Matter
DOI: 10.4230/OASIcs.WPTE.2015.i
Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, and Manfred Schmidt-Schauß

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization
Cite as

2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. i-xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{chiba_et_al:OASIcs.WPTE.2015.i,
  author =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  title =	{{Frontmatter, Table of Contents, Preface, Workshop Organization}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{i--xvi},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.i},
  URN =		{urn:nbn:de:0030-drops-51765},
  doi =		{10.4230/OASIcs.WPTE.2015.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}
Document
Invited Talk
DOI: 10.4230/OASIcs.WPTE.2015.1
Mechanizing Meta-Theory in Beluga (Invited Talk)

Authors: Brigitte Pientka

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will survey the proof environment Beluga. To specify formal systems and represent derivations within them, Beluga provides a sophisticated infrastructure based on the logical framework LF; in particular, its infrastructure not only supports modelling binders via binders in LF, but extends and generalizes LF with first-class contexts to abstract over a set of assumptions, contextual objects to model derivations that depend on assumptions, and first-class simultaneous substitutions to relate contexts. These extensions allow us to directly support key and common concepts that frequently arise when describing formal systems and derivations within them. To reason about formal systems, Beluga provides a dependently typed functional language for implementing inductive proofs about derivations as recursive functions on contextual objects following the Curry-Howard isomorphism. Recently, the Beluga system has also been extended with a totality checker which guarantees that recursive programs are well-founded and correspond to inductive proofs and an interactive program development environment to support incremental proof / program construction. Taken together these extensions enable direct and compact mechanizations. To demonstrate Beluga's strength, we develop a weak normalization proof using logical relations. The Beluga system together with examples is available from http://complogic.cs.mcgill.ca/beluga.
Cite as

Brigitte Pientka. Mechanizing Meta-Theory in Beluga (Invited Talk). In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{pientka:OASIcs.WPTE.2015.1,
  author =	{Pientka, Brigitte},
  title =	{{Mechanizing Meta-Theory in Beluga}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{1--1},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.1},
  URN =		{urn:nbn:de:0030-drops-51770},
  doi =		{10.4230/OASIcs.WPTE.2015.1},
  annote =	{Keywords: Type systems, Dependent Types, Logical Frameworks}
}
Document
DOI: 10.4230/OASIcs.WPTE.2015.3
Head reduction and normalization in a call-by-value lambda-calculus

Authors: Giulio Guerrieri

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
Recently, a standardization theorem has been proven for a variant of Plotkin's call-by-value lambda-calculus extended by means of two commutation rules (sigma-reductions): this result was based on a partitioning between head and internal reductions. We study the head normalization for this call-by-value calculus with sigma-reductions and we relate it to the weak evaluation of original Plotkin's call-by-value lambda-calculus. We give also a (non-deterministic) normalization strategy for the call-by-value lambda-calculus with sigma-reductions.
Cite as

Giulio Guerrieri. Head reduction and normalization in a call-by-value lambda-calculus. In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. 3-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{guerrieri:OASIcs.WPTE.2015.3,
  author =	{Guerrieri, Giulio},
  title =	{{Head reduction and normalization in a call-by-value lambda-calculus}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{3--17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.3},
  URN =		{urn:nbn:de:0030-drops-51789},
  doi =		{10.4230/OASIcs.WPTE.2015.3},
  annote =	{Keywords: sequentialization, lambda-calculus, sigma-reduction, call-by-value, head reduction, internal reduction, (strong) normalization, evaluation, confluence}
}
Document
DOI: 10.4230/OASIcs.WPTE.2015.19
Towards Modelling Actor-Based Concurrency in Term Rewriting

Authors: Adrián Palacios and Germán Vidal

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
In this work, we introduce a scheme for modelling actor systems within sequential term rewriting. In our proposal, a TRS consists of the union of three components: the functional part (which is specific of a system), a set of rules for reducing concurrent actions, and a set of rules for defining a particular scheduling policy. A key ingredient of our approach is that concurrent systems are modelled by terms in which concurrent actions can never occur inside user-defined function calls. This assumption greatly simplifies the definition of the semantics for concurrent actions, since no term traversal will be needed. We prove that these systems are well defined in the sense that concurrent actions can always be reduced. Our approach can be used as a basis for modelling actor-based concurrent programs, which can then be analyzed using existing techniques for term rewrite systems.
Cite as

Adrián Palacios and Germán Vidal. Towards Modelling Actor-Based Concurrency in Term Rewriting. In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. 19-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{palacios_et_al:OASIcs.WPTE.2015.19,
  author =	{Palacios, Adri\'{a}n and Vidal, Germ\'{a}n},
  title =	{{Towards Modelling Actor-Based Concurrency in Term Rewriting}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{19--29},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.19},
  URN =		{urn:nbn:de:0030-drops-51792},
  doi =		{10.4230/OASIcs.WPTE.2015.19},
  annote =	{Keywords: concurrency, actor model, rewriting}
}
Document
DOI: 10.4230/OASIcs.WPTE.2015.31
Observing Success in the Pi-Calculus

Authors: David Sabel and Manfred Schmidt-Schauß

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
A contextual semantics - defined in terms of successful termination and may- and should-convergence - is analyzed in the synchronous pi-calculus with replication and a constant Stop to denote success. The contextual ordering is analyzed, some nontrivial process equivalences are proved, and proof tools for showing contextual equivalences are provided. Among them are a context lemma and new notions of sound applicative similarities for may- and should-convergence. A further result is that contextual equivalence in the pi-calculus with Stop conservatively extends barbed testing equivalence in the (Stop-free) pi-calculus and thus results on contextual equivalence can be transferred to the (Stop-free) pi-calculus with barbed testing equivalence.
Cite as

David Sabel and Manfred Schmidt-Schauß. Observing Success in the Pi-Calculus. In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. 31-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{sabel_et_al:OASIcs.WPTE.2015.31,
  author =	{Sabel, David and Schmidt-Schau{\ss}, Manfred},
  title =	{{Observing Success in the Pi-Calculus}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{31--46},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.31},
  URN =		{urn:nbn:de:0030-drops-51808},
  doi =		{10.4230/OASIcs.WPTE.2015.31},
  annote =	{Keywords: Concurrency, Process calculi, Pi-calculus, Rewriting, Semantics}
}
Document
DOI: 10.4230/OASIcs.WPTE.2015.47
Formalizing Bialgebraic Semantics in PVS 6.0

Authors: Sjaak Smetsers, Ken Madlener, and Marko van Eekelen

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
Both operational and denotational semantics are prominent approaches for reasoning about properties of programs and programming languages. In the categorical framework developed by Turi and Plotkin both styles of semantics are unified using a single, syntax independent format, known as GSOS, in which the operational rules of a language are specified. From this format, the operational and denotational semantics are derived. The approach of Turi and Plotkin is based on the categorical notion of bialgebras. In this paper we specify this work in the theorem prover PVS, and prove the adequacy theorem of this formalization. One of our goals is to investigate whether PVS is adequately suited for formalizing metatheory. Indeed, our experiments show that the original categorical framework can be formalized conveniently. Additionally, we present a GSOS specification for the simple imperative programming language While, and execute the derived semantics for a small example program.
Cite as

Sjaak Smetsers, Ken Madlener, and Marko van Eekelen. Formalizing Bialgebraic Semantics in PVS 6.0. In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. 47-61, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{smetsers_et_al:OASIcs.WPTE.2015.47,
  author =	{Smetsers, Sjaak and Madlener, Ken and van Eekelen, Marko},
  title =	{{Formalizing Bialgebraic Semantics in PVS 6.0}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{47--61},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.47},
  URN =		{urn:nbn:de:0030-drops-51811},
  doi =		{10.4230/OASIcs.WPTE.2015.47},
  annote =	{Keywords: operational semantics, denotational semantics, bialgebras, distributive laws, adequacy, theorem proving, PVS, WHILE}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.WPTE.2014
OASIcs, Volume 40, WPTE'14, Complete Volume

Authors: Manfred Schmidt-Schauß, Masahiko Sakai, David Sabel, and Yuki Chiba

Published in: OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014)

Abstract
OASIcs, Volume 40, WPTE'14, Complete Volume
Cite as

First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Proceedings{schmidtschau_et_al:OASIcs.WPTE.2014,
  title =	{{OASIcs, Volume 40, WPTE'14, Complete Volume}},
  booktitle =	{First International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-70-5},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{40},
  editor =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014},
  URN =		{urn:nbn:de:0030-drops-46216},
  doi =		{10.4230/OASIcs.WPTE.2014},
  annote =	{Keywords: Conference proceedings, Formal Definitions and Theory, Translator writing systems and compiler generators, Specifying and Verifying and Reasoning about Programs, Semantics of Programming Languages, Mathematical Logic, Grammars and Other Rewriting Systems}
}
Document
Front Matter
DOI: 10.4230/OASIcs.WPTE.2014.i
Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Manfred Schmidt-Schauß, Masahiko Sakai, David Sabel, and Yuki Chiba

Published in: OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014)

Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization
Cite as

First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, pp. i-xv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:OASIcs.WPTE.2014.i,
  author =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  title =	{{Frontmatter, Table of Contents, Preface, Workshop Organization}},
  booktitle =	{First International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
  pages =	{i--xv},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-70-5},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{40},
  editor =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014.i},
  URN =		{urn:nbn:de:0030-drops-45814},
  doi =		{10.4230/OASIcs.WPTE.2014.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}
  • Refine by Author
  • 13 Schmidt-Schauß, Manfred
  • 11 Sabel, David
  • 7 Nishida, Naoki
  • 5 Chiba, Yuki
  • 4 Sakai, Masahiko
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Automated reasoning

  • Refine by Keyword
  • 7 term rewriting
  • 4 Rewriting
  • 4 termination
  • 3 Confluence
  • 3 Frontmatter
  • Show More...

  • Refine by Type
  • 56 document
  • 3 volume

  • Refine by Publication Year
  • 33 2011
  • 10 2014
  • 9 2015
  • 3 2013
  • 1 2010
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact