Export Citations
Save this search
Please login to be able to save your searches and receive alerts for new content matching your search criteria.
- research-articleFebruary 2024
Denotational and operational semantics for interaction languages: Application to trace analysis
Science of Computer Programming (SCPR), Volume 232, Issue Chttps://doi.org/10.1016/j.scico.2023.103034AbstractGraphical depictions of distributed systems' behaviors in the form of Sequence Diagrams (SD) are widely used, with formalisms such as Message Sequence Charts (MSC) or UML-SD. Yet, only restricted subsets of these languages are associated to ...
- research-articleJanuary 2024
Forward- or reverse-mode automatic differentiation: What's the difference?
Science of Computer Programming (SCPR), Volume 231, Issue Chttps://doi.org/10.1016/j.scico.2023.103010AbstractAutomatic differentiation (AD) has been a topic of interest for researchers in many disciplines, with increased popularity since its application to machine learning and neural networks. Although many researchers appreciate and know how to apply ...
Highlights- Basic forward mode AD is the fusion of two semiring homomorphisms: symbolic differentiation and evaluation.
- Three fundamental algebraic abstractions lay the foundations of a single-line definition of AD algorithms.
- Different AD ...
- research-articleJanuary 2023
Static analysis of linear absolute value equalities among variables of a program
Science of Computer Programming (SCPR), Volume 225, Issue Chttps://doi.org/10.1016/j.scico.2022.102906AbstractThe classic linear (technically, affine) equality abstract domain, which can infer linear equality relations among variables of a program automatically, is one of the earliest and fundamental abstract domains. However, it cannot ...
Highlights- We propose an abstract domain to infer linear absolute value equalities among program variables.
- research-articleOctober 2022
A decentralized analysis of multiparty protocols
Science of Computer Programming (SCPR), Volume 222, Issue Chttps://doi.org/10.1016/j.scico.2022.102840AbstractProtocols provide the unifying glue in concurrent and distributed software today; verifying that message-passing programs conform to such governing protocols is important but difficult. Static approaches based on multiparty session ...
Highlights
- A new analysis of multiparty protocols expressed as Multiparty Session Types (MPST).
- research-articleMay 2022
Effectful improvement theory
Science of Computer Programming (SCPR), Volume 217, Issue Chttps://doi.org/10.1016/j.scico.2022.102792Highlights- Relational cost theory for effectful functional programming languages.
- Cost as ...
Optimizing programs is hard. Not only one must preserve semantics, but one also needs to ensure that an optimization truly makes the program better. The first part, preserving program semantics, has been, and still is, the subject of ...
-
- research-articleJanuary 2022
Several lifted abstract domains for static analysis of numerical program families
Science of Computer Programming (SCPR), Volume 213, Issue Chttps://doi.org/10.1016/j.scico.2021.102725AbstractLifted (family-based) static analysis based on abstract interpretation is capable of analyzing all variants of a program family (or any other configurable software system), simultaneously, in a single run without ...
- research-articleJune 2020
A formal, scalable approach to semantic interoperability
Science of Computer Programming (SCPR), Volume 192, Issue Chttps://doi.org/10.1016/j.scico.2020.102426AbstractScientific progress is increasingly dependent upon the acquisition, processing, and analysis of large volumes of data. The validity of results and the safety of applications rely upon an adequate understanding of the real-world ...
Highlights- A language for reasoning about semantic interoperability in terms of data models.
- research-articleJune 2020
From CIL to Java bytecode: Semantics-based translation for static analysis leveraging
Science of Computer Programming (SCPR), Volume 191, Issue Chttps://doi.org/10.1016/j.scico.2020.102392Highlights- A formal translation of CIL (.Net) bytecode into Java bytecode is introduced and proved sound w.r.t. the language semantics
A formal translation of CIL (i.e., .Net) bytecode into Java bytecode is introduced and proved sound with respect to the language semantics. The resulting code is then analyzed with Julia, an industrial static analyzer of Java bytecode. ...
- research-articleMay 2020
Bidirectionality in flow-sensitive demand-driven analysis
Science of Computer Programming (SCPR), Volume 190, Issue Chttps://doi.org/10.1016/j.scico.2020.102391AbstractDemand-driven methods for program analysis have primarily been viewed as efficient algorithms for computing the same information as the corresponding exhaustive methods, but for a given set of demands. We explore demand-driven flow-...
- research-articleJanuary 2020
Automated amortised resource analysis for term rewrite systems
Science of Computer Programming (SCPR), Volume 185, Issue Chttps://doi.org/10.1016/j.scico.2019.102306Highlights- We generalise amortised resource analysis to standard rewriting without presupposing termination due to the small step-semantics.
- We overcome earlier restrictions to completely defined, orthogonal, constructor TRSs.
- The analysis ...
In this paper we establish an automated amortised resource analysis for term rewrite systems. The method is presented in an inference system akin to a type-and-effect system and gives rise to polynomial bounds on the innermost runtime complexity ...
- research-articleJune 2019
A type system for first-class layers with inheritance, subtyping, and swapping
Science of Computer Programming (SCPR), Volume 179, Issue CPages 54–86https://doi.org/10.1016/j.scico.2019.03.008AbstractContext-Oriented Programming (COP) is a programming paradigm to encourage modularization of context-dependent software. Key features of COP are layers—modules to describe context-dependent behavioral variations of a software system—and ...
Highlights
- A small calculus of JCop, an extension of Java for Context-Oriented Programming.
- research-articleMarch 2019
A monadic semantics for quantum computing in an object oriented language
Science of Computer Programming (SCPR), Volume 173, Issue CPages 37–55https://doi.org/10.1016/j.scico.2018.03.003AbstractNowadays, several languages and libraries have been proposed to program and reason about quantum programs in the imperative and functional paradigms. Having in mind that the object-oriented paradigm is one of the most used for ...
Highlights- A Monadic Semantics for Quantum Computing inside an Object Oriented Language is proposed.
- research-articleDecember 2018
On the semantics and implementation of replicated data types
Science of Computer Programming (SCPR), Volume 167, Issue CPages 91–113https://doi.org/10.1016/j.scico.2018.06.003Highlights- A replicated data type is specified as a function that maps visibility into admissible arbitrations.
Replicated data types (rdts) concern the specification and implementation of data structures handled by replicated data stores, i.e., distributed data stores that maintain copies of the same data item on multiple devices. A distinctive ...
- research-articleSeptember 2018
Mining inline cache data to order inferred types in dynamic languages
Science of Computer Programming (SCPR), Volume 161, Issue CPages 105–121https://doi.org/10.1016/j.scico.2017.11.003AbstractThe lack of static type information in dynamically-typed languages often poses obstacles for developers. Type inference algorithms can help, but inferring precise type information requires complex algorithms that are often slow.
...Highlights
- An approach to improve the precision of simple type inference is proposed.
- It ...
- research-articleNovember 2016
Specifying and executing optimizations for generalized control flow graphs
Science of Computer Programming (SCPR), Volume 130, Issue CPages 2–23https://doi.org/10.1016/j.scico.2016.06.003Optimizations performed by compilers, usually expressed as rewrites on program graphs, are a core part of modern compilers. However, even production compilers have bugs, and these bugs are difficult to detect and resolve. In this paper we present ...
- research-articleMarch 2016
Improving static analyses of C programs with conditional predicates
Science of Computer Programming (SCPR), Volume 118, Issue CPages 77–95https://doi.org/10.1016/j.scico.2015.11.011Static code analysis is increasingly used to guarantee the absence of undesirable behaviors in industrial programs. Designing sound analyses is a continuing trade-off between precision and complexity. Notably, dataflow analyses often perform overly wide ...
- research-articleJanuary 2016
Parameterized, concurrent session types for asynchronous multi-actor interactions
Science of Computer Programming (SCPR), Volume 115, Issue CPages 100–126https://doi.org/10.1016/j.scico.2015.10.006Session types have been proposed as a means of statically verifying implementations of communication protocols. Although prior work has been successful for some classes of protocols, it does not cope well with parameterized, multi-actor scenarios with ...
- research-articleDecember 2015
A modular specification of Oberon0 using the Silver attribute grammar system
Science of Computer Programming (SCPR), Volume 114, Issue CPages 33–44https://doi.org/10.1016/j.scico.2015.10.009This paper describes an implementation of Oberon0 using the Silver attribute grammar system for the Tool Challenge at the 2011 International Workshop on Language Descriptions, Tools, and Applications. Silver was developed to study how independently-...
- research-articleDecember 2015
Compositional compiler construction
Science of Computer Programming (SCPR), Volume 114, Issue CPages 45–56https://doi.org/10.1016/j.scico.2015.10.008We describe an implementation of an Oberon0 compiler using the techniques proposed in the CoCoCo project. The compiler is constructed out of a collection of pre-compiled, statically type-checked language-definition fragments written in Haskell. Oberon0 ...
- research-articleDecember 2015
Combinators and type-driven transformers in Objective Caml
Science of Computer Programming (SCPR), Volume 114, Issue CPages 57–73https://doi.org/10.1016/j.scico.2015.07.008We describe an implementation of LDTA 2011 Tool Challenge tasks in Objective Caml language. Instead of using some dedicated domain-specific tools we utilize typical functional programming machinery such as polymorphic functions, monads and combinators; ...