Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

Publications by Jorge Sousa Pinto

2000

Sequential and concurrent abstract machines for interaction nets

Authors
Pinto, JS;

Publication
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES

Abstract
This paper is a formal study of how to implement interaction nets, filling an important gap in the work on this graphical rewriting formalism, very promising for the implementation of languages based on the gimel -calculus. We propose the first abstract machine for interaction net reduction, based on a decomposition of interaction rules into more atomic steps, which tackles all the implementation details hidden in the graphical presentation. As a natural extension of this, we then give a concurrent shared-memory abstract machine, and show how to implement it, resulting in the first parallel implementation of interaction nets.

2012

Preface

Authors
Kniesel, G; Pinto, JS;

Publication
Electronic Notes in Theoretical Computer Science

Abstract

2011

Rigorous Software Development - An Introduction to Program Verification

Authors
Almeida, JB; Frade, MJ; Pinto, JS; Sousa, SMd;

Publication
Undergraduate Topics in Computer Science

Abstract

2001

Parallel implementation models for the lambda-calculus using the geometry of interaction

Authors
Pinto, JS;

Publication
TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS

Abstract
An examination of Girard's execution formula suggests implementations of the Geometry of Interaction at the syntactic level. In this paper we limit our scope to ground-type terms and study the parallel aspects of such implementations, by introducing a family of abstract machines which can be directly implemented. These machines address all the important implementation issues such as the choice of an interthread communication model, and allow to incorporate specific strategies for dividing the computation of the execution path into smaller tasks.

2007

A Higher-Order Calculus for Graph Transformation

Authors
Fernandez, M; Mackie, I; Pinto, JS;

Publication
Electronic Notes in Theoretical Computer Science

Abstract
This paper presents a formalism for defining higher-order systems based on the notion of graph transformation (by rewriting or interaction). The syntax is inspired by the Combinatory Reduction Systems of Klop. The rewrite rules can be used to define first-order systems, such as graph or term-graph rewriting systems, Lafont's interaction nets, the interaction systems of Asperti and Laneve, the non-deterministic nets of Alexiev, or a process calculus. They can also be used to specify higher-order systems such as hierarchical graphs and proof nets of Linear Logic, or to specify the operational semantics of graph-based languages.

2012

Assertion-based slicing and slice graphs

Authors
Barros, JB; da Cruz, D; Henriques, PR; Pinto, JS;

Publication
FORMAL ASPECTS OF COMPUTING

Abstract
This paper revisits the idea of slicing programs based on their axiomatic semantics, rather than using criteria based on control/data dependencies. We show how the forward propagation of preconditions and the backward propagation of postconditions can be combined in a new slicing algorithm that is more precise than the existing specification-based algorithms. The algorithm is based on (a) a precise test for removable statements, and (b) the construction of a slice graph, a program control flow graph extended with semantic labels and additional edges that "short-circuit" removable commands. It improves on previous approaches in two aspects: it does not fail to identify removable commands; and it produces the smallest possible slice that can be obtained (in a sense that will be made precise). Iteration is handled through the use of loop invariants and variants to ensure termination. The paper also discusses in detail applications of these forms of slicing, including the elimination of (conditionally) unreachable and dead code, and compares them to other related notions.

  • 7
  • 11