Source author record

Witold Charatonik

Witold Charatonik appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science Programming Languages

Catalog footprint

What is connected

5works

2topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2021arXiv

Strong Call by Value is Reasonable for Time

The invariance thesis of Slot and van Emde Boas states that all reasonable models of computation simulate each other with polynomially bounded overhead in time and constant-factor overhead in space. In this paper we show that a family of strong call-by-value strategies in the $λ$-calculus are reasonable for time. The proof is based on a construction of an appropriate abstract machine, systematically derived using Danvy et al.'s functional correspondence that connects higher-order interpreters with abstract-machine models by a well-established transformation technique. This is the first machine that implements a strong CbV strategy and simulates $β$-reduction with the overhead polynomial in the number of $β$-steps and in the size of the initial term. We prove this property using a form of amortized cost analysis à la Okasaki.

preprint2020arXiv

An Abstract Machine for Strong Call by Value

We present an abstract machine that implements a full-reducing (a.k.a. strong) call-by-value strategy for pure $λ$-calculus. It is derived using Danvy et al.'s functional correspondence from Crégut's KN by: (1) deconstructing KN to a call-by-name normalization-by-evaluation function akin to Filinski and Rohde's, (2) modifying the resulting normalizer so that it implements the right-to-left call-by-value function application, and (3) constructing the functionally corresponding abstract machine. This new machine implements a reduction strategy that subsumes the fireball-calculus variant of call by value studied by Accattoli et al. We describe the strong strategy of the machine in terms of a reduction semantics and prove the correctness of the machine using a method based on Biernacka et al.'s generalized refocusing. As a byproduct, we present an example application of the machine to checking term convertibility by discriminating on the basis of their partially normalized forms.

preprint2016arXiv

Bounded Model Checking of Pointer Programs Revisited

Bounded model checking of pointer programs is a debugging technique for programs that manipulate dynamically allocated pointer structures on the heap. It is based on the following four observations. First, error conditions like dereference of a dangling pointer, are expressible in a~fragment of first-order logic with two-variables. Second, the fragment is closed under weakest preconditions wrt. finite paths. Third, data structures like trees, lists etc. are expressible by inductive predicates defined in a fragment of Datalog. Finally, the combination of the two fragments of the two-variable logic and Datalog is decidable. In this paper we improve this technique by extending the expressivity of the underlying logics. In a~sequence of examples we demonstrate that the new logic is capable of modeling more sophisticated data structures with more complex dependencies on heaps and more complex analyses.

preprint2016arXiv

Extending Two-Variable Logic on Trees

The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.

preprint2014arXiv

Satisfiability of the Two-Variable Fragment of First-Order Logic over Trees

We consider the satisfiability problem for the two-variable fragment of first-order logic over finite unranked trees. We work with signatures consisting of some unary predicates and the binary navigational predicates child, right sibling, and their respective transitive closures. We prove that the satisfiability problem for the logic containing all these predicates is EXPSPACE-complete. Further, we consider the restriction of the class of structures to singular trees, i.e., we assume that at every node precisely one unary predicate holds. We observe that the full logic and even for unordered trees remain EXPSPACE-complete over finite singular trees, but the complexity decreases for some weaker logics. Namely, the logic with one binary predicate, descendant is NEXPTIME-complete, and its guarded version is PSPACE-complete over finite singular trees, even though both these logics are EXPSPACE-complete over arbitrary finite trees.