Marco Devesas Campos

Research Fellow, University of Birmingham

An artist's rendition
An artist's rendition

Bio

I work with Paul Blain Levy on Recursion, guarded recursion and computational effects.

I completed my PhD at the University of Cambridge under the supervision of Prof. Marcelo Fiore. I also hold an MPhil from Cambridge. My first degree was in Systems and Informatics Engineering at Minho University where I specialised in formal methods.

I worked for CERN as a Junior Fellow in the Dashboard project. I also had stints at the Nordic Data Grid Facility, and Philips Research.

If you don't set p{max-width: 30rem;} (or something to that effect) in your webpages we can't be friends.

Contact

Email: m.devesascampos at the department's URL.

Research

My primary preoccupation lies with the Logical foundations of Computer Science. I aim to describe the behaviour of programs through rigorous proof. For that I try to develop both semantical and operational proof techniques capable of handling as wide a range of programming language features as possible. Chief among these features, for its ubiquity, is recursion—in its term, type, guarded, and à la Mendler varieties.

Proofs themselves can be seen as programs—after all, they manipulate the truth of some things into the truth of something else. It’s the “Curry-Howard isomorphism”, as this observation is known, that explains the title of my PhD (“Classical Logic…”). I study how proof systems can influence programming language design and how results about programs can be turned into results about the provability of certain statements.

Publications

Classical Logic with Mendler Induction—A Dual Calculus and its Strong Normalization With Marcelo Fiore. In Logical Foundations of Computer Science (LFCS 2016) Preprint BibTeX DOI Talk

The Algebra of Directed Acyclic Graphs With Marcelo Fiore. In Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky: Essays Dedicated to Samson Abramsky on the Occasion of His 60th Birthday (2013) BibTeX DOI

Implementation of an Orchestration Language as a Haskell Domain Specific Language With Luís Soares Barbosa. In 8th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2009). BibTeX DOI Talk

Talks

Messing with the Future—or the Art of Continuations A lecture aimed at undergraduate students on the continuation passing style of programming and its immense expressive power. Slides (PDF)

Thesis

Mendler Induction and Classical Logic PDF BibTeX
Abstract. This thesis lies at the intersection of two fields: Computer Science and Logic. It follows in the tradition of studies on the Curry-Howard correspondence between types and propositions, and between programs and proofs.

We commence from the Dual Calculus, a language which exhibits interesting computational behaviour by including control effects—the ability for a piece of code to alter its running context. Such manipulations are known to correspond Logically to laws such as Peirce's, the excluded middle, or double negation elimination. For this we dub this language Classical. Our study of the Dual Calculus is guided by a comparative effort between the programming language and Gentzen's related seminal system, the Sequent Calculus; and we refine the (oft presumed) connection between the two. Our discussion is quite general, spanning both propositional—including negation—and quantified types, and, less familiarly, subtractive types.

Next we turn to the reduction rules of the calculus and show that they satisfy several properties: self-duality, substitutivity, subject preservation and, strong normalization—this despite them being non-deterministic and inherently non-confluent. We prove strong normalization by recourse to a very powerful and general realizability argument. Further, we synthesize from our model a lattice structure that is not present in other realizability proofs of strong normalization.

The second half of the thesis focuses on Mendler induction—first in a functional setting, and then within the Dual Calculus. The functional setting serves to motivate and explicate this lesser known form of induction that is, nonetheless, more general than the usual notion—which it subsumes—in that it enables well-founded induction on types with negative occurrences of the induction variable. The definition of the necessary extension of the Dual Calculus follows. Subtractive types are paramount to this definition.

The system thus created is very general, and can embed several other calculi. We show in particular two: the original Mendler inductive (functional) system and a (Classical) Dual Calculus with inductive types. But despite this generality, we still retain the nice reduction behaviour of the of the second-order system—even if this is shown only classically.