17 Search Results for "Sattler, Christian"

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.36
Scaling Interprocedural Static Data-Flow Analysis to Large C/C++ Applications: An Experience Report

Authors: Fabian Schiebel, Florian Sattler, Philipp Dominik Schubert, Sven Apel, and Eric Bodden

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Interprocedural data-flow analysis is important for computing precise information on whole programs. In theory, the popular algorithmic framework interprocedural distributive environments (IDE) provides a tool to solve distributive interprocedural data-flow problems efficiently. Yet, unfortunately, available state-of-the-art implementations of the IDE framework start to run into scalability issues for programs with several thousands of lines of code, depending on the static analysis domain. Since the IDE framework is a basic building block for many static program analyses, this presents a serious limitation. In this paper, we report on our experience with making the IDE algorithm scale to C/C++ applications with up to 500 000 lines of code. We analyze the IDE algorithm and its state-of-the-art implementations to identify their weaknesses related to scalability at both a conceptual and implementation level. Based on this analysis, we propose several optimizations to overcome these weaknesses, aiming at a sweet spot between reducing running time and memory consumption. As a result, we provide an improved IDE solver that implements our optimizations within the PhASAR static analysis framework. Our evaluation on real-world C/C++ applications shows that applying the optimizations speeds up the analysis on average by up to 7×, while also reducing memory consumption by 7× on average as well. For the first time, these optimizations allow us to analyze programs with several hundreds of thousands of lines of LLVM-IR code in reasonable time and space.
Cite as

Fabian Schiebel, Florian Sattler, Philipp Dominik Schubert, Sven Apel, and Eric Bodden. Scaling Interprocedural Static Data-Flow Analysis to Large C/C++ Applications: An Experience Report. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 36:1-36:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{schiebel_et_al:LIPIcs.ECOOP.2024.36,
  author =	{Schiebel, Fabian and Sattler, Florian and Schubert, Philipp Dominik and Apel, Sven and Bodden, Eric},
  title =	{{Scaling Interprocedural Static Data-Flow Analysis to Large C/C++ Applications: An Experience Report}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{36:1--36:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.36},
  URN =		{urn:nbn:de:0030-drops-208859},
  doi =		{10.4230/LIPIcs.ECOOP.2024.36},
  annote =	{Keywords: Interprocedural data-flow analysis, IDE, LLVM, C/C++}
}
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.21
Dynamic Blocked Clause Elimination for Projected Model Counting

Authors: Jean-Marie Lagniez, Pierre Marquis, and Armin Biere

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

Abstract
In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ‖∃ X . Σ‖ of a propositional formula Σ after eliminating a given set X of variables existentially. Although blocked clause elimination is a well-known technique for SAT solving, its direct application to model counting is challenging as in general it changes the number of models. However, we demonstrate, by focusing on projected variables during the blocked clause search, that blocked clause elimination can be leveraged while preserving the correct model count. To take advantage of blocked clause elimination in an efficient way during model counting, a novel data structure and associated algorithms are introduced. Our proposed approach is implemented in the model counter d4. Our experiments demonstrate the computational benefits of our new method of blocked clause elimination for projected model counting.
Cite as

Jean-Marie Lagniez, Pierre Marquis, and Armin Biere. Dynamic Blocked Clause Elimination for Projected Model Counting. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{lagniez_et_al:LIPIcs.SAT.2024.21,
  author =	{Lagniez, Jean-Marie and Marquis, Pierre and Biere, Armin},
  title =	{{Dynamic Blocked Clause Elimination for Projected Model Counting}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{21:1--21:17},
  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.21},
  URN =		{urn:nbn:de:0030-drops-205430},
  doi =		{10.4230/LIPIcs.SAT.2024.21},
  annote =	{Keywords: Projected model counting, blocked clause elimination, propositional logic}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.10
Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics

Authors: Ambrus Kaposi and Szumi Xie

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Programming languages can be defined from the concrete to the abstract by abstract syntax trees, well-scoped syntax, well-typed (intrinsic) syntax, algebraic syntax (well-typed syntax quotiented by conversion). Another aspect is the representation of binding structure for which nominal approaches, De Bruijn indices/levels and higher order abstract syntax (HOAS) are available. In HOAS, binders are given by the function space of an internal language of presheaves. In this paper, we show how to combine the algebraic approach with the HOAS approach: following Uemura, we define languages as second-order generalised algebraic theories (SOGATs). Through a series of examples we show that non-substructural languages can be naturally defined as SOGATs. We give a formal definition of SOGAT signatures (using the syntax of a particular SOGAT) and define two translations from SOGAT signatures to GAT signatures (signatures for quotient inductive-inductive types), based on parallel and single substitutions, respectively.
Cite as

Ambrus Kaposi and Szumi Xie. Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 10:1-10:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.FSCD.2024.10,
  author =	{Kaposi, Ambrus and Xie, Szumi},
  title =	{{Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{10:1--10:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.10},
  URN =		{urn:nbn:de:0030-drops-203396},
  doi =		{10.4230/LIPIcs.FSCD.2024.10},
  annote =	{Keywords: Type theory, universal algebra, inductive types, quotient inductive types, higher-order abstract syntax, logical framework}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.16
On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems

Authors: Franz Baader and Jürgen Giesl

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Motivated by an application where we try to make proofs for Description Logic inferences smaller by rewriting, we consider the following decision problem, which we call the small term reachability problem: given a term rewriting system R, a term s, and a natural number n, decide whether there is a term t of size ≤ n reachable from s using the rules of R. We investigate the complexity of this problem depending on how termination of R can be established. We show that the problem is NP-complete for length-reducing term rewriting systems. Its complexity increases to N2ExpTime-complete (NExpTime-complete) if termination is proved using a (linear) polynomial order and to PSpace-complete for systems whose termination can be shown using a restricted class of Knuth-Bendix orders. Confluence reduces the complexity to P for the length-reducing case, but has no effect on the worst-case complexity in the other two cases.
Cite as

Franz Baader and Jürgen Giesl. On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:LIPIcs.FSCD.2024.16,
  author =	{Baader, Franz and Giesl, J\"{u}rgen},
  title =	{{On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.16},
  URN =		{urn:nbn:de:0030-drops-203454},
  doi =		{10.4230/LIPIcs.FSCD.2024.16},
  annote =	{Keywords: Rewriting, Termination, Confluence, Creating small terms, Derivational complexity, Description Logics, Proof rewriting}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.27
A Verified Algorithm for Deciding Pattern Completeness

Authors: René Thiemann and Akihisa Yamada

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Pattern completeness is the property that the left-hand sides of a functional program cover all cases w.r.t. pattern matching. In the context of term rewriting a related notion is quasi-reducibility, a prerequisite if one wants to perform ground confluence proofs by rewriting induction. In order to certify such confluence proofs, we develop a novel algorithm that decides pattern completeness and that can be used to ensure quasi-reducibility. One of the advantages of the proposed algorithm is its simple structure: it is similar to that of a regular matching algorithm and, unlike an existing decision procedure for quasi-reducibility, it avoids enumerating all terms up to a given depth. Despite the simple structure, proving the correctness of the algorithm is not immediate. Therefore we formalize the algorithm and verify its correctness using the proof assistant Isabelle/HOL. To this end, we not only verify some auxiliary algorithms, but also design an Isabelle library on sorted term rewriting. Moreover, we export the verified code in Haskell and experimentally evaluate its performance. We observe that our algorithm significantly outperforms existing algorithms, even including the pattern completeness check of the GHC Haskell compiler.
Cite as

René Thiemann and Akihisa Yamada. A Verified Algorithm for Deciding Pattern Completeness. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{thiemann_et_al:LIPIcs.FSCD.2024.27,
  author =	{Thiemann, Ren\'{e} and Yamada, Akihisa},
  title =	{{A Verified Algorithm for Deciding Pattern Completeness}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.27},
  URN =		{urn:nbn:de:0030-drops-203566},
  doi =		{10.4230/LIPIcs.FSCD.2024.27},
  annote =	{Keywords: Isabelle/HOL, pattern matching, term rewriting}
}
Document
DOI: 10.4230/DagMan.10.1.1
Current and Future Challenges in Knowledge Representation and Reasoning (Dagstuhl Perspectives Workshop 22282)

Authors: James P. Delgrande, Birte Glimm, Thomas Meyer, Miroslaw Truszczynski, and Frank Wolter

Published in: Dagstuhl Manifestos, Volume 10, Issue 1 (2024)

Abstract
Knowledge Representation and Reasoning is a central, longstanding, and active area of Artificial Intelligence. Over the years it has evolved significantly; more recently it has been challenged and complemented by research in areas such as machine learning and reasoning under uncertainty. In July 2022,sser a Dagstuhl Perspectives workshop was held on Knowledge Representation and Reasoning. The goal of the workshop was to describe the state of the art in the field, including its relation with other areas, its shortcomings and strengths, together with recommendations for future progress. We developed this manifesto based on the presentations, panels, working groups, and discussions that took place at the Dagstuhl Workshop. It is a declaration of our views on Knowledge Representation: its origins, goals, milestones, and current foci; its relation to other disciplines, especially to Artificial Intelligence; and on its challenges, along with key priorities for the next decade.
Cite as

James P. Delgrande, Birte Glimm, Thomas Meyer, Miroslaw Truszczynski, and Frank Wolter. Current and Future Challenges in Knowledge Representation and Reasoning (Dagstuhl Perspectives Workshop 22282). In Dagstuhl Manifestos, Volume 10, Issue 1, pp. 1-61, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{delgrande_et_al:DagMan.10.1.1,
  author =	{Delgrande, James P. and Glimm, Birte and Meyer, Thomas and Truszczynski, Miroslaw and Wolter, Frank},
  title =	{{Current and Future Challenges in Knowledge Representation and Reasoning (Dagstuhl Perspectives Workshop 22282)}},
  pages =	{1--61},
  journal =	{Dagstuhl Manifestos},
  ISSN =	{2193-2433},
  year =	{2024},
  volume =	{10},
  number =	{1},
  editor =	{Delgrande, James P. and Glimm, Birte and Meyer, Thomas and Truszczynski, Miroslaw and Wolter, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagMan.10.1.1},
  URN =		{urn:nbn:de:0030-drops-201403},
  doi =		{10.4230/DagMan.10.1.1},
  annote =	{Keywords: Knowledge representation and reasoning, Applications of logics, Declarative representations, Formal logic}
}
Document
Survey
DOI: 10.4230/TGDK.2.1.3
Semantic Web: Past, Present, and Future

Authors: Ansgar Scherp, Gerd Groener, Petr Škoda, Katja Hose, and Maria-Esther Vidal

Published in: TGDK, Volume 2, Issue 1 (2024): Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge, Volume 2, Issue 1

Abstract
Ever since the vision was formulated, the Semantic Web has inspired many generations of innovations. Semantic technologies have been used to share vast amounts of information on the Web, enhance them with semantics to give them meaning, and enable inference and reasoning on them. Throughout the years, semantic technologies, and in particular knowledge graphs, have been used in search engines, data integration, enterprise settings, and machine learning. In this paper, we recap the classical concepts and foundations of the Semantic Web as well as modern and recent concepts and applications, building upon these foundations. The classical topics we cover include knowledge representation, creating and validating knowledge on the Web, reasoning and linking, and distributed querying. We enhance this classical view of the so-called "Semantic Web Layer Cake" with an update of recent concepts that include provenance, security and trust, as well as a discussion of practical impacts from industry-led contributions. We conclude with an outlook on the future directions of the Semantic Web. This is a living document. If you like to contribute, please contact the first author and visit: https://github.com/ascherp/semantic-web-primer
Cite as

Ansgar Scherp, Gerd Groener, Petr Škoda, Katja Hose, and Maria-Esther Vidal. Semantic Web: Past, Present, and Future. In Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge (TGDK), Volume 2, Issue 1, pp. 3:1-3:37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{scherp_et_al:TGDK.2.1.3,
  author =	{Scherp, Ansgar and Groener, Gerd and \v{S}koda, Petr and Hose, Katja and Vidal, Maria-Esther},
  title =	{{Semantic Web: Past, Present, and Future}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{3:1--3:37},
  ISSN =	{2942-7517},
  year =	{2024},
  volume =	{2},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.2.1.3},
  URN =		{urn:nbn:de:0030-drops-198607},
  doi =		{10.4230/TGDK.2.1.3},
  annote =	{Keywords: Linked Open Data, Semantic Web Graphs, Knowledge Graphs}
}
Document
Survey
DOI: 10.4230/TGDK.2.1.4
Logics for Conceptual Data Modelling: A Review

Authors: Pablo R. Fillottrani and C. Maria Keet

Published in: TGDK, Volume 2, Issue 1 (2024): Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge, Volume 2, Issue 1

Abstract
Information modelling for databases and object-oriented information systems avails of conceptual data modelling languages such as EER and UML Class Diagrams. Many attempts exist to add logical rigour to them, for various reasons and with disparate strengths. In this paper we aim to provide a structured overview of the many efforts. We focus on aims, approaches to the formalisation, including key dimensions of choice points, popular logics used, and the main relevant reasoning services. We close with current challenges and research directions.
Cite as

Pablo R. Fillottrani and C. Maria Keet. Logics for Conceptual Data Modelling: A Review. In Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge (TGDK), Volume 2, Issue 1, pp. 4:1-4:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{fillottrani_et_al:TGDK.2.1.4,
  author =	{Fillottrani, Pablo R. and Keet, C. Maria},
  title =	{{Logics for Conceptual Data Modelling: A Review}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{4:1--4:30},
  ISSN =	{2942-7517},
  year =	{2024},
  volume =	{2},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.2.1.4},
  URN =		{urn:nbn:de:0030-drops-198616},
  doi =		{10.4230/TGDK.2.1.4},
  annote =	{Keywords: Conceptual Data Modelling, EER, UML, Description Logics, OWL}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.18
For the Metatheory of Type Theory, Internal Sconing Is Enough

Authors: Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
Metatheorems about type theories are often proven by interpreting the syntax into models constructed using categorical gluing. We propose to use only sconing (gluing along a global section functor) instead of general gluing. The sconing is performed internally to a presheaf category, and we recover the original glued model by externalization. Our method relies on constructions involving two notions of models: first-order models (with explicit contexts) and higher-order models (without explicit contexts). Sconing turns a displayed higher-order model into a displayed first-order model. Using these, we derive specialized induction principles for the syntax of type theory. The input of such an induction principle is a boilerplate-free description of its motives and methods, not mentioning contexts. The output is a section with computation rules specified in the same internal language. We illustrate our framework by proofs of canonicity and normalization for type theory.
Cite as

Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler. For the Metatheory of Type Theory, Internal Sconing Is Enough. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 18:1-18:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bocquet_et_al:LIPIcs.FSCD.2023.18,
  author =	{Bocquet, Rafa\"{e}l and Kaposi, Ambrus and Sattler, Christian},
  title =	{{For the Metatheory of Type Theory, Internal Sconing Is Enough}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{18:1--18:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.18},
  URN =		{urn:nbn:de:0030-drops-180029},
  doi =		{10.4230/LIPIcs.FSCD.2023.18},
  annote =	{Keywords: type theory, presheaves, canonicity, normalization, sconing, gluing}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2021.6
Internal Strict Propositions Using Point-Free Equations

Authors: István Donkó and Ambrus Kaposi

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

Abstract
The setoid model of Martin-Löf’s type theory bootstraps extensional features of type theory from intensional type theory equipped with a universe of definitionally proof irrelevant (strict) propositions. Extensional features include a Prop-valued identity type with a strong transport rule and function extensionality. We show that a setoid model supporting these features can be defined in intensional type theory without any of these features. The key component is a point-free notion of propositions. Our construction suggests that strict algebraic structures can be defined along the same lines in intensional type theory.
Cite as

István Donkó and Ambrus Kaposi. Internal Strict Propositions Using Point-Free Equations. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{donko_et_al:LIPIcs.TYPES.2021.6,
  author =	{Donk\'{o}, Istv\'{a}n and Kaposi, Ambrus},
  title =	{{Internal Strict Propositions Using Point-Free Equations}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{6:1--6:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.6},
  URN =		{urn:nbn:de:0030-drops-167759},
  doi =		{10.4230/LIPIcs.TYPES.2021.6},
  annote =	{Keywords: Martin-L\"{o}f’s type theory, intensional type theory, function extensionality, setoid model, homotopy type theory}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2019.5
From Cubes to Twisted Cubes via Graph Morphisms in Type Theory

Authors: Gun Pinyo and Nicolai Kraus

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

Abstract
Cube categories are used to encode higher-dimensional categorical structures. They have recently gained significant attention in the community of homotopy type theory and univalent foundations, where types carry the structure of higher groupoids. Bezem, Coquand, and Huber [Bezem et al., 2014] have presented a constructive model of univalence using a specific cube category, which we call the BCH cube category. The higher categories encoded with the BCH cube category have the property that all morphisms are invertible, mirroring the fact that equality is symmetric. This might not always be desirable: the field of directed type theory considers a notion of equality that is not necessarily invertible. This motivates us to suggest a category of twisted cubes which avoids built-in invertibility. Our strategy is to first develop several alternative (but equivalent) presentations of the BCH cube category using morphisms between suitably defined graphs. Starting from there, a minor modification allows us to define our category of twisted cubes. We prove several first results about this category, and our work suggests that twisted cubes combine properties of cubes with properties of globes and simplices (tetrahedra).
Cite as

Gun Pinyo and Nicolai Kraus. From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{pinyo_et_al:LIPIcs.TYPES.2019.5,
  author =	{Pinyo, Gun and Kraus, Nicolai},
  title =	{{From Cubes to Twisted Cubes via Graph Morphisms in Type Theory}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{5:1--5:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.5},
  URN =		{urn:nbn:de:0030-drops-130694},
  doi =		{10.4230/LIPIcs.TYPES.2019.5},
  annote =	{Keywords: homotopy type theory, cubical sets, directed equality, graph morphisms}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.13
Internal Parametricity for Cubical Type Theory

Authors: Evan Cavallo and Robert Harper

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, and we give an account of the identity extension lemma for internal parametricity.
Cite as

Evan Cavallo and Robert Harper. Internal Parametricity for Cubical Type Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cavallo_et_al:LIPIcs.CSL.2020.13,
  author =	{Cavallo, Evan and Harper, Robert},
  title =	{{Internal Parametricity for Cubical Type Theory}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.13},
  URN =		{urn:nbn:de:0030-drops-116564},
  doi =		{10.4230/LIPIcs.CSL.2020.13},
  annote =	{Keywords: parametricity, cubical type theory, higher inductive types}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.11
Homotopy Canonicity for Cubical Type Theory

Authors: Thierry Coquand, Simon Huber, and Christian Sattler

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
Cubical type theory provides a constructive justification of homotopy type theory and satisfies canonicity: every natural number is convertible to a numeral. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. In this paper we show by a sconing argument that if we remove these equations for the path lifting operation from the system, we still retain homotopy canonicity: every natural number is path equal to a numeral.
Cite as

Thierry Coquand, Simon Huber, and Christian Sattler. Homotopy Canonicity for Cubical Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{coquand_et_al:LIPIcs.FSCD.2019.11,
  author =	{Coquand, Thierry and Huber, Simon and Sattler, Christian},
  title =	{{Homotopy Canonicity for Cubical Type Theory}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{11:1--11:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.11},
  URN =		{urn:nbn:de:0030-drops-105188},
  doi =		{10.4230/LIPIcs.FSCD.2019.11},
  annote =	{Keywords: cubical type theory, univalence, canonicity, sconing, Artin glueing}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.25
Gluing for Type Theory

Authors: Ambrus Kaposi, Simon Huber, and Christian Sattler

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
The relationship between categorical gluing and proofs using the logical relation technique is folklore. In this paper we work out this relationship for Martin-Löf type theory and show that parametricity and canonicity arise as special cases of gluing. The input of gluing is two models of type theory and a pseudomorphism between them and the output is a displayed model over the first model. A pseudomorphism preserves the categorical structure strictly, the empty context and context extension up to isomorphism, and there are no conditions on preservation of type formers. We look at three examples of pseudomorphisms: the identity on the syntax, the interpretation into the set model and the global section functor. Gluing along these result in syntactic parametricity, semantic parametricity and canonicity, respectively.
Cite as

Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.FSCD.2019.25,
  author =	{Kaposi, Ambrus and Huber, Simon and Sattler, Christian},
  title =	{{Gluing for Type Theory}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.25},
  URN =		{urn:nbn:de:0030-drops-105323},
  doi =		{10.4230/LIPIcs.FSCD.2019.25},
  annote =	{Keywords: Martin-L\"{o}f type theory, logical relations, parametricity, canonicity, quotient inductive types}
}
  • Refine by Author
  • 4 Kaposi, Ambrus
  • 4 Sattler, Christian
  • 2 Huber, Simon
  • 1 Apel, Sven
  • 1 Baader, Franz
  • Show More...

  • Refine by Classification
  • 7 Theory of computation → Type theory
  • 2 Computing methodologies → Knowledge representation and reasoning
  • 2 Theory of computation → Automated reasoning
  • 2 Theory of computation → Complexity theory and logic
  • 1 Computing methodologies → Artificial intelligence
  • Show More...

  • Refine by Keyword
  • 3 canonicity
  • 2 Description Logics
  • 2 cubical type theory
  • 2 homotopy type theory
  • 2 parametricity
  • Show More...

  • Refine by Type
  • 17 document

  • Refine by Publication Year
  • 9 2024
  • 2 2019
  • 2 2020
  • 1 2011
  • 1 2012
  • 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