13 Search Results for "Traytel, Dmitriy"

Document
DOI: 10.4230/LIPIcs.ITP.2024.12
A Modular Formalization of Superposition in Isabelle/HOL

Authors: Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette, and Sophie Tourret

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Superposition is an efficient proof calculus for reasoning about first-order logic with equality that is implemented in many automatic theorem provers. It works by saturating the given set of clauses and is refutationally complete, meaning that if the set is inconsistent, the saturation will contain a contradiction. In this work, we restructured the completeness proof to cleanly separate the ground (i.e., variable-free) and nonground aspects, and we formalized the result in Isabelle/HOL. We relied on the IsaFoR library for first-order terms and on the Isabelle saturation framework.
Cite as

Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette, and Sophie Tourret. A Modular Formalization of Superposition in Isabelle/HOL. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.ITP.2024.12,
  author =	{Desharnais, Martin and Toth, Balazs and Waldmann, Uwe and Blanchette, Jasmin and Tourret, Sophie},
  title =	{{A Modular Formalization of Superposition in Isabelle/HOL}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.12},
  URN =		{urn:nbn:de:0030-drops-207401},
  doi =		{10.4230/LIPIcs.ITP.2024.12},
  annote =	{Keywords: Superposition, verification, first-order logic, higher-order logic}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.15
Antichain with SAT and Tries

Authors: Lukáš Holík and Pavol Vargovčík

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
We introduce a SAT-enabled version of an antichain algorithm for checking language emptiness of alternating finite automata (AFA) with complex transition relations encoded as compact logical formulae. The SAT solver is used to compute predecessors of AFA configurations, and at the same time, to evaluate the subsumption of newly found configurations in the antichain of the previously found ones. The algorithm could be naively implemented by an incremental SAT solver where the growing antichain is represented by adding new clauses. To make it efficient, we 1) force the SAT solver to prioritize largest/subsumption-strongest predecessors (so that weaker configurations are not even generated), and 2) store the antichain clauses in a special variant of a trie that allows fast subsumption testing. The experimental results suggest that the resulting emptiness checker is very efficient compared to the state of the art and that our techniques improve the performance of the SAT solver.
Cite as

Lukáš Holík and Pavol Vargovčík. Antichain with SAT and Tries. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 15:1-15:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{holik_et_al:LIPIcs.SAT.2024.15,
  author =	{Hol{\'\i}k, Luk\'{a}\v{s} and Vargov\v{c}{\'\i}k, Pavol},
  title =	{{Antichain with SAT and Tries}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{15:1--15:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.15},
  URN =		{urn:nbn:de:0030-drops-205372},
  doi =		{10.4230/LIPIcs.SAT.2024.15},
  annote =	{Keywords: SAT, Trie, Antichain, Alternating automata, Subset query}
}
Document
DOI: 10.4230/OASIcs.FMBC.2024.2
Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda

Authors: Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

Abstract
Blockchain systems comprise critical software that handle substantial monetary funds, rendering them excellent candidates for formal verification. One of their core components is the underlying ledger that does all the accounting: keeping track of transactions and their validity, etc. Unfortunately, previous theoretical studies are typically confined to an idealized setting, while specifications for real implementations are scarce; either the functionality is directly implemented without a proper specification, or at best an informal specification is written on paper. The present work expands beyond prior meta-theoretical investigations of the EUTxO model to encompass the full scale of the Cardano blockchain: our formal specification describes a hierarchy of modular transitions that covers all the intricacies of a realistic blockchain, such as fully expressive smart contracts and decentralized governance. It is mechanized in a proof assistant, thus enjoys a higher standard of rigor: type-checking prevents minor oversights that were frequent in previous informal approaches; key meta-theoretical properties can now be formally proven; it is an executable specification against which the implementation in production is being tested for conformance; and it provides firm foundations for smart contract verification. Apart from a safety net to keep us in check, the formalization also provides a guideline for the ledger design: one informs the other in a symbiotic way, especially in the case of state-of-the-art features like decentralized governance, which is an emerging sub-field of blockchain research that however mandates a more exploratory approach. All the results presented in this paper have been mechanized in the Agda proof assistant and are publicly available. In fact, this document is itself a literate Agda script and all rendered code has been successfully type-checked.
Cite as

Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell. Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{knispel_et_al:OASIcs.FMBC.2024.2,
  author =	{Knispel, Andre and Melkonian, Orestis and Chapman, James and Hill, Alasdair and J\"{a}\"{a}ger, Joosep and DeMeo, William and Norell, Ulf},
  title =	{{Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{2:1--2:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.2},
  URN =		{urn:nbn:de:0030-drops-198673},
  doi =		{10.4230/OASIcs.FMBC.2024.2},
  annote =	{Keywords: blockchain, distributed ledgers, UTxO, Cardano, formal verification, Agda}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.8
Seventeen Provers Under the Hammer

Authors: Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
One of the main success stories of automatic theorem provers has been their integration into proof assistants. Such integrations, or "hammers," increase proof automation and hence user productivity. In this paper, we use Isabelle/HOL’s Sledgehammer tool to find out how useful modern provers are at proving formulas in higher-order logic. Our evaluation follows in the steps of Böhme and Nipkow’s Judgment Day study from 2010, but instead of three provers we use 17, including SMT solvers and higher-order provers. Our work offers an alternative yardstick for comparing modern provers, next to the benchmarks and competitions emerging from the TPTP World and SMT-LIB.
Cite as

Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. Seventeen Provers Under the Hammer. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.ITP.2022.8,
  author =	{Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius},
  title =	{{Seventeen Provers Under the Hammer}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.8},
  URN =		{urn:nbn:de:0030-drops-167178},
  doi =		{10.4230/LIPIcs.ITP.2022.8},
  annote =	{Keywords: Automatic theorem proving, interactive theorem proving, proof assistants}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2022.11
Practical Relational Calculus Query Evaluation

Authors: Martin Raszyk, David Basin, Srđan Krstić, and Dmitriy Traytel

Published in: LIPIcs, Volume 220, 25th International Conference on Database Theory (ICDT 2022)

Abstract
The relational calculus (RC) is a concise, declarative query language. However, existing RC query evaluation approaches are inefficient and often deviate from established algorithms based on finite tables used in database management systems. We devise a new translation of an arbitrary RC query into two safe-range queries, for which the finiteness of the query’s evaluation result is guaranteed. Assuming an infinite domain, the two queries have the following meaning: The first is closed and characterizes the original query’s relative safety, i.e., whether given a fixed database, the original query evaluates to a finite relation. The second safe-range query is equivalent to the original query, if the latter is relatively safe. We compose our translation with other, more standard ones to ultimately obtain two SQL queries. This allows us to use standard database management systems to evaluate arbitrary RC queries. We show that our translation improves the time complexity over existing approaches, which we also empirically confirm in both realistic and synthetic experiments.
Cite as

Martin Raszyk, David Basin, Srđan Krstić, and Dmitriy Traytel. Practical Relational Calculus Query Evaluation. In 25th International Conference on Database Theory (ICDT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 220, pp. 11:1-11:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{raszyk_et_al:LIPIcs.ICDT.2022.11,
  author =	{Raszyk, Martin and Basin, David and Krsti\'{c}, Sr{\d}an and Traytel, Dmitriy},
  title =	{{Practical Relational Calculus Query Evaluation}},
  booktitle =	{25th International Conference on Database Theory (ICDT 2022)},
  pages =	{11:1--11:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-223-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{220},
  editor =	{Olteanu, Dan and Vortmeier, Nils},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2022.11},
  URN =		{urn:nbn:de:0030-drops-158857},
  doi =		{10.4230/LIPIcs.ICDT.2022.11},
  annote =	{Keywords: Relational calculus, relative safety, safe-range, query translation}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.10
Verified Progress Tracking for Timely Dataflow

Authors: Matthias Brun, Sára Decova, Andrea Lattuada, and Dmitriy Traytel

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
Large-scale stream processing systems often follow the dataflow paradigm, which enforces a program structure that exposes a high degree of parallelism. The Timely Dataflow distributed system supports expressive cyclic dataflows for which it offers low-latency data- and pipeline-parallel stream processing. To achieve high expressiveness and performance, Timely Dataflow uses an intricate distributed protocol for tracking the computation’s progress. We modeled the progress tracking protocol as a combination of two independent transition systems in the Isabelle/HOL proof assistant. We specified and verified the safety of the two components and of the combined protocol. To this end, we identified abstract assumptions on dataflow programs that are sufficient for safety and were not previously formalized.
Cite as

Matthias Brun, Sára Decova, Andrea Lattuada, and Dmitriy Traytel. Verified Progress Tracking for Timely Dataflow. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{brun_et_al:LIPIcs.ITP.2021.10,
  author =	{Brun, Matthias and Decova, S\'{a}ra and Lattuada, Andrea and Traytel, Dmitriy},
  title =	{{Verified Progress Tracking for Timely Dataflow}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{10:1--10:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.10},
  URN =		{urn:nbn:de:0030-drops-139057},
  doi =		{10.4230/LIPIcs.ITP.2021.10},
  annote =	{Keywords: safety, distributed systems, timely dataflow, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.5
Efficient Full Higher-Order Unification

Authors: Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
We developed a procedure to enumerate complete sets of higher-order unifiers based on work by Jensen and Pietrzykowski. Our procedure removes many redundant unifiers by carefully restricting the search space and tightly integrating decision procedures for fragments that admit a finite complete set of unifiers. We identify a new such fragment and describe a procedure for computing its unifiers. Our unification procedure is implemented in the Zipperposition theorem prover. Experimental evaluation shows a clear advantage over Jensen and Pietrzykowski’s procedure.
Cite as

Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin. Efficient Full Higher-Order Unification. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{vukmirovic_et_al:LIPIcs.FSCD.2020.5,
  author =	{Vukmirovi\'{c}, Petar and Bentkamp, Alexander and Nummelin, Visa},
  title =	{{Efficient Full Higher-Order Unification}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.5},
  URN =		{urn:nbn:de:0030-drops-123271},
  doi =		{10.4230/LIPIcs.FSCD.2020.5},
  annote =	{Keywords: unification, higher-order logic, theorem proving, term rewriting, indexing data structures}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.6
Data Types as Quotients of Polynomial Functors

Authors: Jeremy Avigad, Mario Carneiro, and Simon Hudon

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
A broad class of data types, including arbitrary nestings of inductive types, coinductive types, and quotients, can be represented as quotients of polynomial functors. This provides perspicuous ways of constructing them and reasoning about them in an interactive theorem prover.
Cite as

Jeremy Avigad, Mario Carneiro, and Simon Hudon. Data Types as Quotients of Polynomial Functors. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{avigad_et_al:LIPIcs.ITP.2019.6,
  author =	{Avigad, Jeremy and Carneiro, Mario and Hudon, Simon},
  title =	{{Data Types as Quotients of Polynomial Functors}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.6},
  URN =		{urn:nbn:de:0030-drops-110612},
  doi =		{10.4230/LIPIcs.ITP.2019.6},
  annote =	{Keywords: data types, polynomial functors, inductive types, coinductive types}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.10
Generic Authenticated Data Structures, Formally

Authors: Matthias Brun and Dmitriy Traytel

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
Authenticated data structures are a technique for outsourcing data storage and maintenance to an untrusted server. The server is required to produce an efficiently checkable and cryptographically secure proof that it carried out precisely the requested computation. Recently, Miller et al. [https://doi.org/10.1145/2535838.2535851] demonstrated how to support a wide range of such data structures by integrating an authentication construct as a first class citizen in a functional programming language. In this paper, we put this work to the test of formalization in the Isabelle proof assistant. With Isabelle’s help, we uncover and repair several mistakes and modify the small-step semantics to perform call-by-value evaluation rather than requiring terms to be in administrative normal form.
Cite as

Matthias Brun and Dmitriy Traytel. Generic Authenticated Data Structures, Formally. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brun_et_al:LIPIcs.ITP.2019.10,
  author =	{Brun, Matthias and Traytel, Dmitriy},
  title =	{{Generic Authenticated Data Structures, Formally}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.10},
  URN =		{urn:nbn:de:0030-drops-110657},
  doi =		{10.4230/LIPIcs.ITP.2019.10},
  annote =	{Keywords: Authenticated Data Structures, Verifiable Computation, Isabelle/HOL, Nominal Isabelle}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.127
From Nondeterministic to Multi-Head Deterministic Finite-State Transducers (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Martin Raszyk, David Basin, and Dmitriy Traytel

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
Every nondeterministic finite-state automaton is equivalent to a deterministic finite-state automaton. This result does not extend to finite-state transducers - finite-state automata equipped with a one-way output tape. There is a strict hierarchy of functions accepted by one-way deterministic finite-state transducers (1DFTs), one-way nondeterministic finite-state transducers (1NFTs), and two-way nondeterministic finite-state transducers (2NFTs), whereas the two-way deterministic finite-state transducers (2DFTs) accept the same family of functions as their nondeterministic counterparts (2NFTs). We define multi-head one-way deterministic finite-state transducers (mh-1DFTs) as a natural extension of 1DFTs. These transducers have multiple one-way reading heads that move asynchronously over the input word. Our main result is that mh-1DFTs can deterministically express any function defined by a one-way nondeterministic finite-state transducer. Of independent interest, we formulate the all-suffix regular matching problem, which is the problem of deciding for each suffix of an input word whether it belongs to a regular language. As part of our proof, we show that an mh-1DFT can solve all-suffix regular matching, which has applications, e.g., in runtime verification.
Cite as

Martin Raszyk, David Basin, and Dmitriy Traytel. From Nondeterministic to Multi-Head Deterministic Finite-State Transducers (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 127:1-127:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{raszyk_et_al:LIPIcs.ICALP.2019.127,
  author =	{Raszyk, Martin and Basin, David and Traytel, Dmitriy},
  title =	{{From Nondeterministic to Multi-Head Deterministic Finite-State Transducers}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{127:1--127:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.127},
  URN =		{urn:nbn:de:0030-drops-107037},
  doi =		{10.4230/LIPIcs.ICALP.2019.127},
  annote =	{Keywords: Formal languages, Nondeterminism, Multi-head automata, Finite transducers}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.11
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL

Authors: Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
We present a collection of formalized results about finite nested multisets, developed using the Isabelle/HOL proof assistant. The nested multiset order is a generalization of the multiset order that can be used to prove termination of processes. Hereditary multisets, a variant of nested multisets, offer a convenient representation of ordinals below epsilon-0. In Isabelle/HOL, both nested and hereditary multisets can be comfortably defined as inductive datatypes. Our formal library also provides, somewhat nonstandardly, multisets with negative multiplicities and syntactic ordinals with negative coefficients. We present applications of the library to formalizations of Goodstein's theorem and the decidability of unary PCF (programming computable functions).
Cite as

Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel. Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{blanchette_et_al:LIPIcs.FSCD.2017.11,
  author =	{Blanchette, Jasmin Christian and Fleury, Mathias and Traytel, Dmitriy},
  title =	{{Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{11:1--11:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.11},
  URN =		{urn:nbn:de:0030-drops-77155},
  doi =		{10.4230/LIPIcs.FSCD.2017.11},
  annote =	{Keywords: Multisets, ordinals, proof assistants}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.31
Formal Languages, Formally and Coinductively

Authors: Dmitriy Traytel

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
Traditionally, formal languages are defined as sets of words. More recently, the alternative coalgebraic or coinductive representation as infinite tries, i.e., prefix trees branching over the alphabet, has been used to obtain compact and elegant proofs of classic results in language theory. In this paper, we study this representation in the Isabelle proof assistant. We define regular operations on infinite tries and prove the axioms of Kleene algebra for those operations. Thereby, we exercise corecursion and coinduction and confirm the coinductive view being profitable in formalizations, as it improves over the set-of-words view with respect to proof automation.
Cite as

Dmitriy Traytel. Formal Languages, Formally and Coinductively. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{traytel:LIPIcs.FSCD.2016.31,
  author =	{Traytel, Dmitriy},
  title =	{{Formal Languages, Formally and Coinductively}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{31:1--31:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.31},
  URN =		{urn:nbn:de:0030-drops-59853},
  doi =		{10.4230/LIPIcs.FSCD.2016.31},
  annote =	{Keywords: Formal languages, codatatypes, corecursion, coinduction, interactive theorem proving, Isabelle HOL}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.487
A Coalgebraic Decision Procedure for WS1S

Authors: Dmitriy Traytel

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

Abstract
Weak monadic second-order logic of one successor (WS1S) is a simple and natural formalism to specify regular properties. WS1S is decidable, although the decision procedure's complexity is non-elementary. Typically, decision procedures for WS1S exploit the logic-automaton connection, i.e. they escape the simple and natural formalism by translating formulas into equally expressive regular structures such as finite automata, regular expressions, or games. In this work, we devise a coalgebraic decision procedure for WS1S that stays within the logical world by directly operating on formulas. The key operation is the derivative of a formula, modeled after Brzozowski's derivatives of regular expressions. The presented decision procedure has been formalized and proved correct in the interactive proof assistant Isabelle.
Cite as

Dmitriy Traytel. A Coalgebraic Decision Procedure for WS1S. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 487-503, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{traytel:LIPIcs.CSL.2015.487,
  author =	{Traytel, Dmitriy},
  title =	{{A Coalgebraic Decision Procedure for WS1S}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{487--503},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.487},
  URN =		{urn:nbn:de:0030-drops-54335},
  doi =		{10.4230/LIPIcs.CSL.2015.487},
  annote =	{Keywords: WS1S, decision procedure, coalgebra, Brzozowski derivatives, Isabelle}
}
  • Refine by Author
  • 7 Traytel, Dmitriy
  • 2 Basin, David
  • 2 Blanchette, Jasmin
  • 2 Brun, Matthias
  • 2 Desharnais, Martin
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 Formal languages
  • 2 Isabelle/HOL
  • 2 higher-order logic
  • 2 interactive theorem proving
  • 2 proof assistants
  • Show More...

  • Refine by Type
  • 13 document

  • Refine by Publication Year
  • 3 2019
  • 3 2024
  • 2 2022
  • 1 2015
  • 1 2016
  • 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact