Search Results

Documents authored by Kuncak, Viktor

Document
DOI: 10.4230/LIPIcs.ITP.2024.18
Mechanized HOL Reasoning in Set Theory

Authors: Simon Guilloud, Sankalp Gambhir, Andrea Gilot, and Viktor Kunčak

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

Abstract
We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADTs) into first-order logic with ZFC axioms. Our approach interprets types as sets, with function (arrow) types coinciding with set-theoretic function spaces. We assume traditional FOL syntax without notation for term-level binders. To embed λ-terms, we define a notion of context, defining the closure of all abstractions occuring inside a term. We implement the embedding in the Lisa proof assistant for schematic first-order logic and its library based on axiomatic set theory (presented at ITP 2023). We show how to implement type checking and the proof steps of HOL Light as proof-producing tactics in Lisa. The embedded HOL theorems and proofs are interoperable with the existing Lisa library. This yields a form of soft type system supporting top-level polymorphism and ADTs within set theory. The approach offers tools for Lisa users to carry HOL-style proofs within set theory. It also enables the import of HOL Light theorem statements into Lisa, as well as the replay of small HOL Light kernel proofs.
Cite as

Simon Guilloud, Sankalp Gambhir, Andrea Gilot, and Viktor Kunčak. Mechanized HOL Reasoning in Set Theory. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{guilloud_et_al:LIPIcs.ITP.2024.18,
  author =	{Guilloud, Simon and Gambhir, Sankalp and Gilot, Andrea and Kun\v{c}ak, Viktor},
  title =	{{Mechanized HOL Reasoning in Set Theory}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{18:1--18:18},
  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.18},
  URN =		{urn:nbn:de:0030-drops-207464},
  doi =		{10.4230/LIPIcs.ITP.2024.18},
  annote =	{Keywords: Proof assistant, First Order Logic, Set Theory, Higher Order Logic}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.17
LISA - A Modern Proof System

Authors: Simon Guilloud, Sankalp Gambhir, and Viktor Kunčak

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and function symbols. It implements polynomial-time proof checking and uses the axioms of ortholattices (which implies the irrelevance of the order of conjuncts and disjuncts and additional propositional laws). The kernel supports the notion of theorems (whose proofs are not expanded), as well as definitions of predicate symbols and objects whose unique existence is proven. A domain-specific language enables construction of proofs and development of proof tactics with user-friendly tools and presentation, while remaining within the general-purpose language, Scala. We describe the LISA proof system and illustrate the flavour and the level of abstraction of proofs written in LISA. This includes a proof-generating tactic for propositional tautologies, leveraging the ortholattice properties to reduce the size of proofs. We also present early formalization of set theory in LISA, including Cantor’s theorem.
Cite as

Simon Guilloud, Sankalp Gambhir, and Viktor Kunčak. LISA - A Modern Proof System. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{guilloud_et_al:LIPIcs.ITP.2023.17,
  author =	{Guilloud, Simon and Gambhir, Sankalp and Kun\v{c}ak, Viktor},
  title =	{{LISA - A Modern Proof System}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{17:1--17:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.17},
  URN =		{urn:nbn:de:0030-drops-183922},
  doi =		{10.4230/LIPIcs.ITP.2023.17},
  annote =	{Keywords: Proof assistant, First Order Logic, Set Theory}
}
Document
DOI: 10.4230/DARTS.3.2.16
Proactive Synthesis of Recursive Tree-to-String Functions from Examples (Artifact)

Authors: Mikaël Mayer, Jad Hamza, and Viktor Kuncak

Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
This artifact, named Prosy, is an interactive command-line tool for synthesizing recursive tree-to-string functions (e.g. pretty-printers) from examples. Specifically, Prosy takes as input a Scala file containing a hierarchy of abstract and case classes, and synthesizes the printing function after interacting with the user. Prosy first pro-actively generates a finite set of trees such that their string representations uniquely determine the function to synthesize. While asking the output for each example, Prosy prunes away questions when it can infer their answers from previous answers. In the companion paper, we prove that this pruning allows Prosy not to require that the user provides answers to the entire set of questions, which is of size O(n^3) where n is the size of the input file, but only to a reasonably small subset of size O(n). Furthermore, Prosy guides the interaction by providing suggestions whenever it can.
Cite as

Mikaël Mayer, Jad Hamza, and Viktor Kuncak. Proactive Synthesis of Recursive Tree-to-String Functions from Examples (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 16:1-16:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{mayer_et_al:DARTS.3.2.16,
  author =	{Mayer, Mika\"{e}l and Hamza, Jad and Kuncak, Viktor},
  title =	{{Proactive Synthesis of Recursive Tree-to-String Functions from Examples (Artifact)}},
  pages =	{16:1--16:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Mayer, Mika\"{e}l and Hamza, Jad and Kuncak, Viktor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.16},
  URN =		{urn:nbn:de:0030-drops-72970},
  doi =		{10.4230/DARTS.3.2.16},
  annote =	{Keywords: programming by example, active learning, program synthesis}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2017.19
Proactive Synthesis of Recursive Tree-to-String Functions from Examples

Authors: Mikaël Mayer, Jad Hamza, and Viktor Kuncak

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
Synthesis from examples enables non-expert users to generate programs by specifying examples of their behavior. A domain-specific form of such synthesis has been recently deployed in a widely used spreadsheet software product. In this paper we contribute to foundations of such techniques and present a complete algorithm for synthesis of a class of recursive functions defined by structural recursion over a given algebraic data type definition. The functions we consider map an algebraic data type to a string; they are useful for, e.g., pretty printing and serialization of programs and data. We formalize our problem as learning deterministic sequential top-down tree-to-string transducers with a single state (1STS). The first problem we consider is learning a tree-to-string transducer from any set of input/output examples provided by the user. We show that, given a set of input/output examples, checking whether there exists a 1STS consistent with these examples is NP-complete in general. In contrast, the problem can be solved in polynomial time under a (practically useful) closure condition that each subtree of a tree in the input/output example set is also part of the input/output examples. Because coming up with relevant input/output examples may be difficult for the user while creating hard constraint problems for the synthesizer, we also study a more automated active learning scenario in which the algorithm chooses the inputs for which the user provides the outputs. Our algorithm asks a worst-case linear number of queries as a function of the size of the algebraic data type definition to determine a unique transducer. To construct our algorithms we present two new results on formal languages. First, we define a class of word equations, called sequential word equations, for which we prove that satisfiability can be solved in deterministic polynomial time. This is in contrast to the general word equations for which the best known complexity upper bound is in linear space. Second, we close a long-standing open problem about the asymptotic size of test sets for context-free languages. A test set of a language of words L is a subset T of L such that any two word homomorphisms equivalent on T are also equivalent on L. We prove that it is possible to build test sets of cubic size for context-free languages, matching for the first time the lower bound found 20 years ago.
Cite as

Mikaël Mayer, Jad Hamza, and Viktor Kuncak. Proactive Synthesis of Recursive Tree-to-String Functions from Examples. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 19:1-19:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{mayer_et_al:LIPIcs.ECOOP.2017.19,
  author =	{Mayer, Mika\"{e}l and Hamza, Jad and Kuncak, Viktor},
  title =	{{Proactive Synthesis of Recursive Tree-to-String Functions from Examples}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{19:1--19:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.19},
  URN =		{urn:nbn:de:0030-drops-72575},
  doi =		{10.4230/LIPIcs.ECOOP.2017.19},
  annote =	{Keywords: programming by example, active learning, program synthesis}
}
Document
DOI: 10.4230/DagSemProc.05431.4
On Algorithms and Complexity for Sets with Cardinality Constraints

Authors: Viktor Kuncak, Martin Rinard, and Bruno Marnette

Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)

Abstract
Complexity of data structures in modern programs presents a challenge for current analysis and verification tools, forcing them to report false alarms or miss errors. I will describe a new approach for verifying programs with complex data structures. This approach builds on program analysis techniques, as well as decision procedures and theorem provers. The approach is based on specifying interfaces of data structures by writing procedure preconditions and postconditions in terms of abstract sets and relations. Our system then separately verifies that 1) each data structure conforms to its interface, 2) each data structure interface is used correctly, and 3) desired high-level application-specific invariants hold. The system verifies these conditions by combining decision procedures, theorem provers, and static analyses, promising an unprecedented tradeoff between precision and scalability. In the context of this system, we have developed new decision procedures for reasoning about sets and their cardinalities, approaches for extending the applicability of existing decision procedures, and techniques for modular analysis of dynamically created data structure instances.
Cite as

Viktor Kuncak, Martin Rinard, and Bruno Marnette. On Algorithms and Complexity for Sets with Cardinality Constraints. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{kuncak_et_al:DagSemProc.05431.4,
  author =	{Kuncak, Viktor and Rinard, Martin and Marnette, Bruno},
  title =	{{On Algorithms and Complexity for Sets with Cardinality Constraints}},
  booktitle =	{Deduction and Applications},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.4},
  URN =		{urn:nbn:de:0030-drops-5125},
  doi =		{10.4230/DagSemProc.05431.4},
  annote =	{Keywords: Static analysis, data structure consistency, program verification, decision procedures}
}
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