11 Search Results for "Czajka, Lukasz"

Document
DOI: 10.4230/LIPIcs.ITP.2024.10
Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory

Authors: Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad

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

Abstract
We present Duper, a proof-producing theorem prover for Lean based on the superposition calculus. Duper can be called directly as a terminal tactic in interactive Lean proofs, but is also designed with proof reconstruction for a future Lean hammer in mind. In this paper, we describe Duper’s underlying approach to proof search and proof reconstruction with a particular emphasis on the challenges of working in a dependent type theory. We also compare Duper’s performance to Metis' on pre-existing benchmarks to give evidence that Duper is performant enough to be useful for proof reconstruction in a hammer.
Cite as

Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad. Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{clune_et_al:LIPIcs.ITP.2024.10,
  author =	{Clune, Joshua and Qian, Yicheng and Bentkamp, Alexander and Avigad, Jeremy},
  title =	{{Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{10:1--10: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.10},
  URN =		{urn:nbn:de:0030-drops-207381},
  doi =		{10.4230/LIPIcs.ITP.2024.10},
  annote =	{Keywords: proof search, automatic theorem proving, interactive theorem proving, Lean, dependent type theory}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2023.2
Finite Combinatory Logic with Predicates

Authors: Andrej Dudenhefner, Christoph Stahl, Constantin Chaumet, Felix Laarmann, and Jakob Rehof

Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)

Abstract
Type inhabitation in extensions of Finite Combinatory Logic (FCL) is the mechanism underlying various component-oriented synthesis frameworks. In FCL inhabitant sets correspond to regular tree languages and vice versa. Therefore, it is not possible to specify non-regular properties of inhabitants, such as (dis)equality of subterms. Additionally, the monomorphic nature of FCL oftentimes hinders concise specification of components. We propose a conservative extension to FCL by quantifiers and predicates, introducing a restricted form of polymorphism. In the proposed type system (FCLP) inhabitant sets correspond to decidable term languages and vice versa. As a consequence, type inhabitation in FCLP is undecidable. Based on results in tree automata theory, we identify a fragment of FCLP with the following two properties. First, the fragment enjoys decidable type inhabitation. Second, it allows for specification of local (dis)equality constraints for subterms of inhabitants. For empirical evaluation, we implement a semi-decision procedure for type inhabitation in FCLP. We compare specification capabilities, scalability, and performance of the implementation to existing FCL-based approaches. Finally, we evaluate practical applicability via a case study, synthesizing mechanically sound robotic arms.
Cite as

Andrej Dudenhefner, Christoph Stahl, Constantin Chaumet, Felix Laarmann, and Jakob Rehof. Finite Combinatory Logic with Predicates. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 2:1-2:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2023.2,
  author =	{Dudenhefner, Andrej and Stahl, Christoph and Chaumet, Constantin and Laarmann, Felix and Rehof, Jakob},
  title =	{{Finite Combinatory Logic with Predicates}},
  booktitle =	{29th International Conference on Types for Proofs and Programs (TYPES 2023)},
  pages =	{2:1--2:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-332-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{303},
  editor =	{Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.2},
  URN =		{urn:nbn:de:0030-drops-204808},
  doi =		{10.4230/LIPIcs.TYPES.2023.2},
  annote =	{Keywords: combinatory logic, inhabitation, intersection types, program synthesis}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ITP.2023.2
Interactive and Automated Proofs in Modal Separation Logic (Invited Talk)

Authors: Robbert Krebbers

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

Abstract
In program verification, it is common to embed a high-level object logic into the meta logic of a proof assistant to hide low-level aspects of the verification. To verify imperative and concurrent programs, separation logic hides explicit reasoning about heaps and pointer disjointness. To verify programs with cyclic features such as modules or higher-order state, modal logic provides modalities to hide explicit reasoning about step-indices that are used to stratify recursion. The meta logic of proof assistants such as Coq is well suited to embed high-level object logics and prove their soundness. However, proof assistants such as Coq do not have native infrastructure to facilitate proofs in embedded logics - their proof contexts and built-in tactics for interactive and automated proofs are tailored to the connectives of the meta logic, and do not extend to those of the object logic. This results in proofs that are at a too low level of abstraction because they are cluttered with bookkeeping code related to manipulating the object logic. In this talk I will describe our work in the Iris project to address this problem - first for interactive proofs, and then for semi-automated proofs. The Iris Proof Mode provides high-level tactics for interactive proofs in higher-order concurrent separation logic with modalities. Recent work on RefinedC and Diaframe have built on top of the Iris Proof Mode to obtain proof automation for low-level C programs and fine-grained concurrent programs.
Cite as

Robbert Krebbers. Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{krebbers:LIPIcs.ITP.2023.2,
  author =	{Krebbers, Robbert},
  title =	{{Interactive and Automated Proofs in Modal Separation Logic}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{2:1--2:1},
  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.2},
  URN =		{urn:nbn:de:0030-drops-183770},
  doi =		{10.4230/LIPIcs.ITP.2023.2},
  annote =	{Keywords: Program Verification, Separation Logic, Step-Indexing, Modal Logic, Interactive Theorem Proving, Proof Automation, Iris, Coq}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.14
Restricting Tree Grammars with Term Rewriting

Authors: Jan Bessai, Lukasz Czajka, Felix Laarmann, and Jakob Rehof

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

Abstract
We investigate the problem of enumerating all terms generated by a tree-grammar which are also in normal form with respect to a set of directed equations (rewriting relation). To this end we show that deciding emptiness and finiteness of the resulting set is EXPTIME-complete. The emptiness result is inspired by a prior result by Comon and Jacquemard on ground reducibility. The finiteness result is based on modification of pumping arguments used by Comon and Jacquemard. We highlight practical applications and limitations. We provide and evaluate a prototype implementation. Limitations are somewhat surprising in that, while deciding emptiness and finiteness is EXPTIME-complete for linear and nonlinear rewrite relations, the linear case is practically feasible while the nonlinear case is infeasible, even for a trivially small example. The algorithms provided for the linear case also improve on prior practical results by Kallat et al.
Cite as

Jan Bessai, Lukasz Czajka, Felix Laarmann, and Jakob Rehof. Restricting Tree Grammars with Term Rewriting. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bessai_et_al:LIPIcs.FSCD.2022.14,
  author =	{Bessai, Jan and Czajka, Lukasz and Laarmann, Felix and Rehof, Jakob},
  title =	{{Restricting Tree Grammars with Term Rewriting}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{14:1--14:19},
  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.14},
  URN =		{urn:nbn:de:0030-drops-162953},
  doi =		{10.4230/LIPIcs.FSCD.2022.14},
  annote =	{Keywords: tree automata, tree grammar, term rewriting, normalization, emptiness, finiteness}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.14
First-Order Guarded Coinduction in Coq

Authors: Łukasz Czajka

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

Abstract
We introduce two coinduction principles and two proof translations which, under certain conditions, map coinductive proofs that use our principles to guarded Coq proofs. The first principle provides an "operational" description of a proof by coinduction, which is easy to reason with informally. The second principle extends the first one to allow for direct proofs by coinduction of statements with existential quantifiers and multiple coinductive predicates in the conclusion. The principles automatically enforce the correct use of the coinductive hypothesis. We implemented the principles and the proof translations in a Coq plugin.
Cite as

Łukasz Czajka. First-Order Guarded Coinduction in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{czajka:LIPIcs.ITP.2019.14,
  author =	{Czajka, {\L}ukasz},
  title =	{{First-Order Guarded Coinduction in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{14:1--14: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.14},
  URN =		{urn:nbn:de:0030-drops-110690},
  doi =		{10.4230/LIPIcs.ITP.2019.14},
  annote =	{Keywords: coinduction, Coq, guardedness, corecursion}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.12
Polymorphic Higher-Order Termination

Authors: Łukasz Czajka and Cynthia Kop

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

Abstract
We generalise the termination method of higher-order polynomial interpretations to a setting with impredicative polymorphism. Instead of using weakly monotonic functionals, we interpret terms in a suitable extension of System F_omega. This enables a direct interpretation of rewrite rules which make essential use of impredicative polymorphism. In addition, our generalisation eases the applicability of the method in the non-polymorphic setting by allowing for the encoding of inductive data types. As an illustration of the potential of our method, we prove termination of a substantial fragment of full intuitionistic second-order propositional logic with permutative conversions.
Cite as

Łukasz Czajka and Cynthia Kop. Polymorphic Higher-Order Termination. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{czajka_et_al:LIPIcs.FSCD.2019.12,
  author =	{Czajka, {\L}ukasz and Kop, Cynthia},
  title =	{{Polymorphic Higher-Order Termination}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{12:1--12:18},
  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.12},
  URN =		{urn:nbn:de:0030-drops-105193},
  doi =		{10.4230/LIPIcs.FSCD.2019.12},
  annote =	{Keywords: termination, polymorphism, higher-order rewriting, permutative conversions}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2016.9
A Shallow Embedding of Pure Type Systems into First-Order Logic

Authors: Lukasz Czajka

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract
We define a shallow embedding of logical proof-irrelevant Pure Type Systems (piPTSs) into minimal first-order logic. In logical piPTSs a distinguished sort *^p of propositions is assumed. Given a context Gamma and a Gamma-proposition tau, i.e., a term tau such that Gamma |- tau : *^p, the embedding translates tau and Gamma into a first-order formula F_Gamma(tau) and a set of first-order axioms Delta_Gamma. The embedding is not complete in general, but it is strong enough to correctly translate most of piPTS propositions (by completeness we mean that if Gamma |- M : tau is derivable in the piPTS then F_Gamma(tau) is provable in minimal first-order logic from the axioms Delta_Gamma). We show the embedding to be sound, i.e., if F_Gamma(tau) is provable in minimal first-order logic from the axioms Delta_Gamma, then Gamma |- M : tau is derivable in the original system for some term M. The interest in the proposed embedding stems from the fact that it forms a basis of the translations used in the recently developed CoqHammer automation tool for dependent type theory.
Cite as

Lukasz Czajka. A Shallow Embedding of Pure Type Systems into First-Order Logic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 9:1-9:39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{czajka:LIPIcs.TYPES.2016.9,
  author =	{Czajka, Lukasz},
  title =	{{A Shallow Embedding of Pure Type Systems into First-Order Logic}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{9:1--9:39},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.9},
  URN =		{urn:nbn:de:0030-drops-98533},
  doi =		{10.4230/LIPIcs.TYPES.2016.9},
  annote =	{Keywords: pure type systems, first-order logic, hammers, proof automation, dependent type theory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.13
Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data

Authors: Lukasz Czajka

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

Abstract
We show that LOGSPACE is characterised by finite orthogonal tail-recursive cons-free constructor term rewriting systems, contributing to a line of research initiated by Neil Jones. We describe a LOGSPACE algorithm which computes constructor normal forms. This algorithm is used in the proof of our main result: that simple stream term rewriting systems characterise LOGSPACE-computable stream functions as defined by Ramyaa and Leivant. This result concerns characterising logarithmic-space computation on infinite streams by means of infinitary rewriting.
Cite as

Lukasz Czajka. Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{czajka:LIPIcs.FSCD.2018.13,
  author =	{Czajka, Lukasz},
  title =	{{Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{13:1--13:19},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.13},
  URN =		{urn:nbn:de:0030-drops-91831},
  doi =		{10.4230/LIPIcs.FSCD.2018.13},
  annote =	{Keywords: LOGSPACE, implicit complexity, term rewriting, infinitary rewriting, streams}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.14
Confluence of an Extension of Combinatory Logic by Boolean Constants

Authors: Lukasz Czajka

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

Abstract
We show confluence of a conditional term rewriting system CL-pc^1, which is an extension of Combinatory Logic by Boolean constants. This solves problem 15 from the RTA list of open problems. The proof has been fully formalized in the Coq proof assistant.
Cite as

Lukasz Czajka. Confluence of an Extension of Combinatory Logic by Boolean Constants. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 14:1-14:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{czajka:LIPIcs.FSCD.2017.14,
  author =	{Czajka, Lukasz},
  title =	{{Confluence of an Extension of Combinatory Logic by Boolean Constants}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{14:1--14:16},
  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.14},
  URN =		{urn:nbn:de:0030-drops-77368},
  doi =		{10.4230/LIPIcs.FSCD.2017.14},
  annote =	{Keywords: combinatory logic, conditional linearization, unique normal form property, confluence}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.106
Confluence of nearly orthogonal infinitary term rewriting systems

Authors: Lukasz Czajka

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
We give a relatively simple coinductive proof of confluence, modulo equivalence of root-active terms, of nearly orthogonal infinitary term rewriting systems. Nearly orthogonal systems allow certain root overlaps, but no non-root overlaps. Using a slightly more complicated method we also show confluence modulo equivalence of hypercollapsing terms. The condition we impose on root overlaps is similar to the condition used by Toyama in the context of finitary rewriting.
Cite as

Lukasz Czajka. Confluence of nearly orthogonal infinitary term rewriting systems. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 106-126, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{czajka:LIPIcs.RTA.2015.106,
  author =	{Czajka, Lukasz},
  title =	{{Confluence of nearly orthogonal infinitary term rewriting  systems}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{106--126},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.106},
  URN =		{urn:nbn:de:0030-drops-51929},
  doi =		{10.4230/LIPIcs.RTA.2015.106},
  annote =	{Keywords: infinitary rewriting, confluence, coinduction}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.174
A Semantic Approach to Illative Combinatory Logic

Authors: Lukasz Czajka

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
This work introduces the theory of illative combinatory algebras, which is closely related to systems of illative combinatory logic. We thus provide a semantic interpretation for a formal framework in which both logic and computation may be expressed in a unified manner. Systems of illative combinatory logic consist of combinatory logic extended with constants and rules of inference intended to capture logical notions. Our theory does not correspond strictly to any traditional system, but draws inspiration from many. It differs from them in that it couples the notion of truth with the notion of equality between terms, which enables the use of logical formulas in conditional expressions. We give a consistency proof for first-order illative combinatory algebras. A complete embedding of classical predicate logic into our theory is also provided. The translation is very direct and natural.
Cite as

Lukasz Czajka. A Semantic Approach to Illative Combinatory Logic. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 174-188, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{czajka:LIPIcs.CSL.2011.174,
  author =	{Czajka, Lukasz},
  title =	{{A Semantic Approach to Illative Combinatory Logic}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{174--188},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.174},
  URN =		{urn:nbn:de:0030-drops-32303},
  doi =		{10.4230/LIPIcs.CSL.2011.174},
  annote =	{Keywords: illative combinatory logic, term rewriting, first-order logic}
}
  • Refine by Author
  • 6 Czajka, Lukasz
  • 2 Czajka, Łukasz
  • 2 Laarmann, Felix
  • 2 Rehof, Jakob
  • 1 Avigad, Jeremy
  • Show More...

  • Refine by Classification
  • 4 Theory of computation → Type theory
  • 3 Theory of computation → Equational logic and rewriting
  • 2 Theory of computation → Automated reasoning
  • 2 Theory of computation → Logic and verification
  • 1 Theory of computation → Automata extensions
  • Show More...

  • Refine by Keyword
  • 3 term rewriting
  • 2 Coq
  • 2 coinduction
  • 2 combinatory logic
  • 2 confluence
  • Show More...

  • Refine by Type
  • 11 document

  • Refine by Publication Year
  • 2 2018
  • 2 2019
  • 2 2024
  • 1 2011
  • 1 2015
  • 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