BZPEERReading, trust and collaboration for researchDiscover
Workspaces
Network
Opportunities
Account
Researcher profile
Alejandro Ríos contributes to research discovery and scholarly infrastructure.
Trust snapshot
Actions
Identity and collaboration
Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.
Log in to claimDirect collaboration
Claim this author entity first to unlock direct invitations.
Research graph
Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.
BZPEER is loading the nearby papers, people, topics and institutions for this page.
Published work
We show that call-by-need is observationally equivalent to weak-head needed reduction. The proof of this result uses a semantical argument based on a (non-idempotent) intersection type system called $\mathcal{V}$. Interestingly, system $\mathcal{V}$ also allows to syntactically identify all the weak-head needed redexes of a term.
We generalize the notion of proof term to the realm of transfinite reduction. Proof terms represent reductions in the first-order term format, thereby facilitating their formal analysis. We show that any transfinite reduction can be faithfully represented as an infinitary proof term, which is unique up to, infinitary, associativity. Our main use of proof terms is in a definition of permutation equivalence for transfinite reductions, on the basis of permutation equations. This definition involves a variant of equational logic, adapted for dealing with infinite objects. A proof of the compression property via proof terms is presented, which establishes permutation equivalence between the original and the compressed reductions.
This work gives some insights and results on standardisation for call-by-name pattern calculi. More precisely, we define standard reductions for a pattern calculus with constructor-based data terms and patterns. This notion is based on reduction steps that are needed to match an argument with respect to a given pattern. We prove the Standardisation Theorem by using the technique developed by Takahashi and Crary for lambda-calculus. The proof is based on the fact that any development can be specified as a sequence of head steps followed by internal reductions, i.e. reductions in which no head steps are involved.
This article is devoted to the presentation of lambda_rex, an explicit substitution calculus with de Bruijn indexes and a simple notation. By being isomorphic to lambda_ex - a recent formalism with variable names -, lambda_rex accomplishes simulation of beta-reduction (Sim), preservation of beta-strong normalization (PSN) and meta-confluence (MC), among other desirable properties. Our calculus is based on a novel presentation of lambda_dB, using a swap notion that was originally devised by de Bruijn. Besides lambda_rex, two other indexed calculi isomorphic to lambda_x and lambda_xgc are presented, demonstrating the potential of our technique when applied to the design of indexed versions of known named calculi.