arXiv subjects

Alan Schmitt

Publications and source records attributed to Alan Schmitt.

7 recordsLinked to original sources

arXiv2024

Fully Abstract Encodings of $λ$-Calculus in HOcore through Abstract Machines

We present fully abstract encodings of the call-by-name and call-by-value $λ$-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the $λ$-calculus side -- normal-form bisimilarity, applicative bisimilarity, and contextual equivalence -- that we internalize into abstract machines in order to prove full abstraction of the encodings. We also demonstrate that this technique scales to the $λμ$-calculus, i.e., a standard extension of the $λ$-calculus with control operators.

cs.LO↗

arXiv2023

Deriving Abstract Interpreters from Skeletal Semantics

This paper describes a methodology for defining an executable abstract interpreter from a formal description of the semantics of a programming language. Our approach is based on Skeletal Semantics and an abstract interpretation of its semantic meta-language. The correctness of the derived abstract interpretation can be established by compositionality provided that correctness properties of the core language-specific constructs are established. We illustrate the genericness of our method by defining a Value Analysis for a small imperative language based on its skeletal semantics.

cs.PL↗

arXiv2018

Skeletal Semantics and their Interpretations

The development of mechanised language specification based on structured operational semantics, with applications to verified compilers and sound program analysis, requires huge effort. General theory and frameworks have been proposed to help with this effort. However, none of this work provides a systematic way of developing concrete and abstract semantics, connected together by a general consistency result. We introduce a skeletal semantics of a language, where each skeleton describes the complete semantic behaviour of a language construct. We define a general notion of interpretation, which provides a systematic and language-independent way of deriving semantic judgements from the skeletal semantics. We explore four generic interpretations: a simple well-formedness interpretation; a concrete interpretation; an abstract interpretation; and a constraint generator for flow-sensitive analysis. We prove general consistency results between interpretations, depending only on simple language-dependent lemmas. We illustrate our ideas using a simple While language.

cs.PL↗

arXiv2013

Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version)

We present a technique for deriving semantic program analyses from a natural semantics specification of the programming language. The technique is based on a particular kind of semantics called pretty-big-step semantics. We present a pretty-big-step semantics of a language with simple objects called O'While and specify a series of instrumentations of the semantics that explicitates the flows of values in a program. This leads to a semantics-based dependency analysis, at the core, e.g., of tainting analysis in software security. The formalization has been realized with the Coq proof assistant.

cs.PL↗

arXiv2013

Proceedings of the 14th International Symposium on Database Programming Languages (DBPL 2013), August 30, 2013, Riva del Garda, Trento, Italy

This volume contains the papers presented at the 14th Symposium on Database Programming Languages (DBPL 2013) held on August 30th, 2013, in Riva del Garda, co-located with the 39th International Conference on Very Large Databases (VLDB 2013). They cover a wide range of topics including the application of programming language techniques to further the expressiveness of database languages, schema management, and the practical use of XPath. To complement this technical program, DBPL 2013 featured three invited talks by Serge Abiteboul (Inria), Jérôme Siméon (IBM), and Soren Lassen (Facebook).

cs.DB↗

arXiv2010

On the Count of Trees

Regular tree grammars and regular path expressions constitute core constructs widely used in programming languages and type systems. Nevertheless, there has been little research so far on frameworks for reasoning about path expressions where node cardinality constraints occur along a path in a tree. We present a logic capable of expressing deep counting along paths which may include arbitrary recursive forward and backward navigation. The counting extensions can be seen as a generalization of graded modalities that count immediate successor nodes. While the combination of graded modalities, nominals, and inverse modalities yields undecidable logics over graphs, we show that these features can be combined in a decidable tree logic whose main features can be decided in exponential time. Our logic being closed under negation, it may be used to decide typical problems on XPath queries such as satisfiability, type checking with relation to regular types, containment, or equivalence.

cs.DB↗

arXiv2010

A Tree Logic with Graded Paths and Nominals

Regular tree grammars and regular path expressions constitute core constructs widely used in programming languages and type systems. Nevertheless, there has been little research so far on reasoning frameworks for path expressions where node cardinality constraints occur along a path in a tree. We present a logic capable of expressing deep counting along paths which may include arbitrary recursive forward and backward navigation. The counting extensions can be seen as a generalization of graded modalities that count immediate successor nodes. While the combination of graded modalities, nominals, and inverse modalities yields undecidable logics over graphs, we show that these features can be combined in a tree logic decidable in exponential time.

cs.LO↗