Search

Your search keyword '"Schubert, Aleksy"' showing total 137 results
Start Over Author "Schubert, Aleksy"
137 results on '"Schubert, Aleksy"'

1. Between proof construction and SAT-solving

Author

Schubert, Aleksy, Urzyczyn, Paweł, and Zdanowski, Konrad

Subjects
Computer Science - Logic in Computer Science
Abstract

The classical satisfiability problem (SAT) is used as a natural and general tool to express and solve combinatorial problems that are in NP. We postulate that provability for implicational intuitionistic propositional logic (IIPC) can serve as a similar natural tool to express problems in Pspace. This approach can be particularly convenient for two reasons. One is that provability in full IPC (with all connectives) can be reduced to provability of implicational formulas of order three. Another advantage is a convenient interpretation in terms of simple alternating automata. Additionally, we distinguish some natural subclasses of IIPC corresponding to the complexity classes NP and co-NP. Our experimental results show that a simple decision procedure requires a significant amount of time only in a small fraction of cases.

Published
2024

2. On non-structural subtype entailment

Author

Schubert, Aleksy

Subjects
Computer Science - Programming Languages
Abstract

We prove that the non-structural subtype entailment problem for finite and regular type expressions is in PSPACE. In this way we close a decidability and complexity gap pending since 1996., Comment: The paper contains error in formulation of Lemma 5.5, which invalidates the further construction

Published
2021

3. Formalisation of a frame stack semantics for a Java-like language

Author

Schubert, Aleksy and Chrząszcz, Jacek

Subjects
Computer Science - Logic in Computer Science, D.3.2, D.3.3, D.1.1, D.1.5, F.3.2
Abstract

We present a Coq formalisation of the small-step operational semantics of Jafun, a small Java-like language with classes. This format of semantics makes it possible to naturally specify and prove invariants that should hold at each computation step. In contrast to the Featherweight Java approach the semantics explicitly manipulates frame stack of method calls. Thanks to that one can express properties of computation that depend on execution of particular methods. On the basis of the semantics, we developed a type system that makes it possible to delineate a notion of a compound value and classify certain methods as extensional functions operating on them. In our formalisation we make a mechanised proof that the operational semantics for the untyped version of the semantics agrees with the one for the typed one. We discuss different methods to make such formalisation effort and provide experiments that substantiate it., Comment: Pre-proceedings paper presented at the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), Frankfurt am Main, Germany, 4-6 September 2018 (arXiv:1808.03326)

Published
2018

4. First-order answer set programming as constructive proof search

Author

Schubert, Aleksy and Urzyczyn, Paweł

Subjects
Computer Science - Logic in Computer Science
Abstract

We propose an interpretation of the first-order answer set programming (FOASP) in terms of intuitionistic proof theory. It is obtained by two polynomial translations between FOASP and the bounded-arity fragment of the Sigma_1 level of the Mints hierarchy in first-order intuitionistic logic. It follows that Sigma_1 formulas using predicates of fixed arity (in particular unary) is of the same strength as FOASP. Our construction reveals a close similarity between constructive provability and stable entailment, or equivalently, between the construction of an answer set and an intuitionistic refutation. This paper is under consideration for publication in Theory and Practice of Logic Programming, Comment: Paper presented at the 34nd International Conference on Logic Programming (ICLP 2018), Oxford, UK, July 14 to July 17, 2018 18 pages, LaTeX (arXiv:1804.10004)

Published
2018

5. On the Mints Hierarchy in First-Order Intuitionistic Logic

Author

Schubert, Aleksy, Urzyczyn, Paweł, and Zdanowski, Konrad

Subjects
Computer Science - Logic in Computer Science
Abstract

We stratify intuitionistic first-order logic over $(\forall,\to)$ into fragments determined by the alternation of positive and negative occurrences of quantifiers (Mints hierarchy). We study the decidability and complexity of these fragments. We prove that even the $\Delta_2$ level is undecidable and that $\Sigma_1$ is Expspace-complete. We also prove that the arity-bounded fragment of $\Sigma_1$ is complete for co-Nexptime.

Published
2016
Full Text
View/download PDF

7. Automata Theory Approach to Predicate Intuitionistic Logic

Author

Zielenkiewicz, Maciej and Schubert, Aleksy

Subjects
Computer Science - Logic in Computer Science, F.1.1, F.4.3
Abstract

Predicate intuitionistic logic is a well established fragment of dependent types. According to the Curry-Howard isomorphism proof construction in the logic corresponds well to synthesis of a program the type of which is a given formula. We present a model of automata that can handle proof construction in full intuitionistic first-order logic. The automata are constructed in such a way that any successful run corresponds directly to a normal proof in the logic. This makes it possible to discuss formal languages of proofs or programs, the closure properties of the automata and their connections with the traditional logical connectives., Comment: Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)

Published
2016

8. Lucretia - intersection type polymorphism for scripting languages

Author

Benke, Marcin, Bono, Viviana, and Schubert, Aleksy

Subjects
Computer Science - Logic in Computer Science, Computer Science - Programming Languages, F.3.3, F.4.1
Abstract

Scripting code may present maintenance problems in the long run. There is, then, the call for methodologies that make it possible to control the properties of programs written in dynamic languages in an automatic fashion. We introduce Lucretia, a core language with an introspection primitive. Lucretia is equipped with a (retrofitted) static type system based on local updates of types that describe the structure of objects being used. In this way, we deal with one of the most dynamic features of scripting languages, that is, the runtime modification of object interfaces. Judgements in our systems have a Hoare-like shape, as they have a precondition and a postcondition part. Preconditions describe static approximations of the interfaces of visible objects before a certain expression has been executed and postconditions describe them after its execution. The field update operation complicates the issue of aliasing in the system. We cope with it by introducing intersection types in method signatures., Comment: In Proceedings ITRS 2014, arXiv:1503.04377

Published
2015
Full Text
View/download PDF

9. On multiply-exponential write-once Turing machines

Author

Zielenkiewicz, Maciej, Schubert, Aleksy, and Chrząszcz, Jacek

Subjects
Computer Science - Computational Complexity, Computer Science - Formal Languages and Automata Theory, F.1.1, F.1.3
Abstract

In this work we analyze the multiply-exponential complexity classes for write-once Turing machines, i.e. machines that can write to a given tape cell at most once. We show that $k$-DExpWOSpace = $k$-DExpWOTime = $k$-ExpTime and the nondeterministic counterpart. For alternating machines we show that $k$-AExpWOTime = $k$-AExpTime = $k-1$-ExpSpace.

Published
2014

10. A Java Bytecode Formalisation

Author

Czarnik, Patryk, Chrząszcz, Jacek, Schubert, Aleksy, Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Weikum, Gerhard, Series Editor, Piskac, Ruzica, editor, and Rümmer, Philipp, editor

Published
2018
Full Text
View/download PDF

11. Lucretia - a type system for objects in languages with reflection

Author

Bono, Viviana, Benke, Marcin, and Schubert, Aleksy

Subjects
Computer Science - Programming Languages, Computer Science - Logic in Computer Science, F.3.3, F.4.1
Abstract

Object-oriented scripting languages such as JavaScript or Python gain in popularity due to their flexibility. Still, the growing code bases written in the languages call for methods that make possible to automatically control the properties of the programs that ensure their stability in the running time. We propose a type system, called Lucretia, that makes possible to control the object structure of languages with reflection. Subject reduction and soundness of the type system with respect to the semantics of the language is proved., Comment: 21 pages

Published
2012

12. Automata Theory Approach to Predicate Intuitionistic Logic

Author

Zielenkiewicz, Maciej, Schubert, Aleksy, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Hermenegildo, Manuel V, editor, and Lopez-Garcia, Pedro, editor

Published
2017
Full Text
View/download PDF

14. On the Mints Hierarchy in First-Order Intuitionistic Logic

Author

Schubert, Aleksy, Urzyczyn, Paweł, Zdanowski, Konrad, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, and Pitts, Andrew, editor

Published
2015
Full Text
View/download PDF

15. Java Loops Are Mainly Polynomial

Author

Zielenkiewicz, Maciej, Chrząszcz, Jacek, Schubert, Aleksy, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Italiano, Giuseppe F., editor, Margaria-Steffen, Tiziana, editor, Pokorný, Jaroslav, editor, Quisquater, Jean-Jacques, editor, and Wattenhofer, Roger, editor

Published
2015
Full Text
View/download PDF

17. Tool Support for Teaching Hoare Logic

Author

Sznuk, Tadeusz, Schubert, Aleksy, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Giannakopoulou, Dimitra, editor, and Salaün, Gwen, editor

Published
2014
Full Text
View/download PDF

18. The Role of Polymorphism in the Characterisation of Complexity by Soft Types

Author

Chrząszcz, Jacek, Schubert, Aleksy, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Murlak, Filip, editor, and Sankowski, Piotr, editor

Published
2011
Full Text
View/download PDF

20. BML and Related Tools

Author

Chrząszcz, Jacek, Huisman, Marieke, Schubert, Aleksy, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, de Boer, Frank S., editor, Bonsangue, Marcello M., editor, and Madelaine, Eric, editor

Published
2009
Full Text
View/download PDF

21. The Existential Fragment of the One-Step Parallel Rewriting Theory

Author

Schubert, Aleksy, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Treinen, Ralf, editor

Published
2009
Full Text
View/download PDF

22. Existential Type Systems with No Types in Terms

Author

Fujita, Ken-etsu, Schubert, Aleksy, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Curien, Pierre-Louis, editor

Published
2009
Full Text
View/download PDF

23. Extending Operational Semantics of the Java Bytecode

Author

Czarnik, Patryk, Schubert, Aleksy, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Barthe, Gilles, editor, and Fournet, Cédric, editor

Published
2008
Full Text
View/download PDF

27. A Self-dependency Constraint in the Simply Typed Lambda Calculus

Author

Schubert, Aleksy, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Liśkiewicz, Maciej, editor, and Reischuk, Rüdiger, editor

Published
2005
Full Text
View/download PDF

36. Automata theory approach to predicate intuitionistic logic.

Author

Zielenkiewicz, Maciej and Schubert, Aleksy

Subjects
PREDICATE (Logic), FIRST-order logic, ISOMORPHISM (Mathematics), FORMAL languages, ROBOTS
Abstract

Predicate intuitionistic logic is a well-established fragment of dependent types. Proof construction in this logic, as the Curry–Howard isomorphism states, is the process of program synthesis. We present automata that can handle proof construction and program synthesis in full intuitionistic first-order logic. Given a formula, we can construct an automaton such that the formula is provable if and only if the automaton has an accepting run. As further research, this construction makes it possible to discuss formal languages of proofs or programs, the closure properties of the automata and their connections with the traditional logical connectives. [ABSTRACT FROM AUTHOR]

Published
2022
Full Text
View/download PDF

41. Preface

Author

Altenkirch, Thorsten, primary and Schubert, Aleksy, additional

Published
2019
Full Text
View/download PDF

47. Coq Support in HAHA

Author

Chrzaszcz, Jacek, Schubert, Aleksy, and Zakrzewski, Jakub

Subjects
000 Computer science, knowledge, general works, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science
Abstract

HAHA is a tool that helps in teaching and learning Hoare logic. It is targeted at an introductory course on software verification. We present a set of new features of the HAHA verification environment that exploit Coq. These features are (1) generation of verification conditions in Coq so that they can be explored and proved interactively and (2) compilation of HAHA programs into CompCert certified compilation tool-chain. With the interactive Coq proving support we obtain an interesting functionality that makes it possible to carefully examine step-by-step verification conditions and systematically discover flaws in their formulation. As a result Coq back-end serves as a kind of specification debugger.

Published
2018
Full Text
View/download PDF

50. Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic

Author

Benke, Marcin, Schubert, Aleksy, and Walukiewicz-Chrzaszcz, Daria

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 000 Computer science, knowledge, general works, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Computer Science, Computer Science::Programming Languages
Abstract

Curry-Howard isomorphism makes it possible to obtain functional programs from proofs in logic. We analyse the problem of program synthesis for ML programs with algebraic types and relate it to the proof search problems in appropriate logics. The problem of synthesis for closed programs is easily equivalent to the proof construction in intuitionistic propositional logic and thus fits in the class of PSPACE-complete problems. We focus further attention on the synthesis problem relative to a given external library of functions. It turns out that the problem is undecidable for unbounded instantiation in ML. However its restriction to instantiations with atomic types only results in a case equivalent to proof search in a restricted fragment of intuitionistic first-order logic, being the core of Sigma_1 level of the logic in the Mints hierarchy. This results in EXPSPACE-completeness for this special case of the ML program synthesis problem.

Published
2016
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results