A
constructive interpretation of Ramsey's theorem via the product of
selection functions
Paulo
Oliva
and Thomas Powell
[pdf] Submitted for publication, December
2011
On
Spector's bar recursion
Paulo
Oliva
and Thomas Powell
[pdf] Submitted for publication, December
2011
On
the relation between various negative translations Gilda Ferreira
and Paulo Oliva
[pdf] Submitted for publication, July
2011
Bar
recursion and products of selection functions Martín Escardó Paulo Oliva
[pdf] Submitted for publication, November
2010
A
Hoare logic for linear systems Rob
Arthan and Ursula
Martin and Paulo Oliva
[pdf] To appear: Formal Aspects of Computing, 2011
The
Pierce translation Martín Escardó Paulo Oliva
[pdf] To appear in: Annals of Pure and Applied
Logic, 2011
On
bounded functional interpretations Gilda Ferreira
and Paulo Oliva
[pdf] To appear in: Annals of Pure and Applied
Logic, 2011
System
T
and
the
product
of
selection
functions Martín Escardó, Paulo Oliva and Thomas Powell
[pdf] Proceedings of Computer Science Logic
(CSL), 2011
Sequential
games
and
optimal
strategies Martín Escardó and Paulo Oliva
[pdf] Proceedings of the Royal
Society A,
467:1519-1545, 2011
Functional
interpretations
of
intuitionistic
linear
logic Gilda Ferreira and Paulo Oliva
[pdf] Logical
Methods
in
Computer
Science, 7(1):paper09, March 2011
(extended version of homonymous CSL'09 invited talk/abstract)
What
sequential games, the Tychnoff theorem and the double-negation shift
have in common Martín Escardó and Paulo Oliva
[pdf] Proceedings
of
MSFP
2010,
ACM
SIGPLAN
Mathematically
Structured
Functional Programming, 21-32,
2010
Hybrid
functional
interpretations
of
linear
and
intuitionistic
logic
Paulo
Oliva
[pdf] Journal of Logic
and Computation, online,
Feb
2010
On
various negative translations
(version in proceeding does not contain proofs. See pdf below for
extended version) Gilda Ferreira
and Paulo Oliva
[pdf] Proceedings
of
Classical
Logic
and
Computation,2010
Proof
interpretations
with
truth Jaime Gaspar and Paulo
Oliva
[pdf] Mathematical
Logic
Quarterly, 56(6):591-610, 2010
Functional
interpretations
of
linear
and
intuitionistic
logic
Paulo
Oliva
[pdf] Information
and
Computation, 208(5):565-577,
2010
Searchable
sets,
Dubuc-Penon
compactness,
omniscience
principles,
and
the
drinker
paradox Martín Escardó and
Paulo Oliva
[pdf] Proceedings
of
CiE'2010
The
Peirce translation and the double negation shift Martín Escardó and Paulo Oliva
[pdf] Proceedings
of
CiE
2010,
LNCS 6158:151-161, 2010
Computational
interpretations
of
analysis
via
products
of
selection
functions Martín Escardó and Paulo Oliva
[pdf] Proceedings
of
CiE
2010, LNCS
6158:141-150, 2010
Selection
functions,
bar
recursion
and
backward
induction Martín Escardó and Paulo Oliva
[pdf] Mathematical
Structures
in
Computer
Science,20(2):127-168,
2010
Confined
modified
realizability Gilda Ferreira and Paulo Oliva
[pdf] Mathematical
Logic
Quarterly, 56(1):13-28, 2010
A
general framework for sound and complete Floyd-Hoare logics Rob
Arthan, Ursula Martin,
Erik
Arne
Mathiesen
and
Paulo
Oliva
[pdf] ACM
Transactions
of
Computational
Logic, 11(1):1-31, 2009
Functional
interpretations
of
intuitionistic
linear
logic Gilda Ferreira and Paulo Oliva
[pdf] Proceedings
of
CSL'09,
LNCS 5771:3-19,
Springer, 2009
Hybrid
functional
interpretations Mircea-Dan Hernest and
Paulo Oliva
[pdf] Proceedings of CiE'08, LNCS
5028:251-260, Springer, 2008
An
analysis of Gödel's dialectica interpretation via linear logic
Paulo
Oliva
[pdf] dialectica, 62:269-290, 2008
On
Krivine's realizability interpretation of classical second-order
arithmetic
Paulo
Oliva
and
Thomas
Streicher
[pdf] Fundamenta Informaticae, 84(2):207-220,
2008
Reasoning
about
linear
systems Rob
Arthan, Ursula Martin,
Erik
Arne
Mathiesen
and
Paulo
Oliva
[pdf] Proceedings
of
SEFM,
2007
Computational
interpretations
of
classical
linear
logic
(extended
abstract
of
invited
talk:
not
peer-reviewed)
Paulo
Oliva
[pdf] Proceedings
of WoLLIC'07, LNCS 4576:285-296, 2007
Modified
realizability
interpretation
of
classical
linear
logic
Paulo Oliva
[pdf] Proceedings
of LICS, 431-440, 2007
Bounded
functional
interpretation
and
feasible
analysis Fernando
Ferreira and Paulo Oliva
[pdf] Annals of Pure
and Applied Logic, 145(2):115-129,
2007
Hoare
logic
in
the
abstract Ursula
Martin,
Erik
Arne
Mathiesen and Paulo Oliva
[pdf] Proceedings
of CSL'2006, LNCS 4207:501-515, Springer, 2006
Understanding
and
using
Spector's
bar
recursive
interpretation
of
classical
analysis
Paulo
Oliva
[pdf] Proceedings of
CiE'2006, LNCS 3988:423-434, Springer, 2006
Unifying
functional
interpretations
Paulo Oliva
[pdf] Notre Dame Journal of Formal
Logic, 47(2):263-290, 2006
Modified
bar
recursion Ulrich Berger
and Paulo Oliva
[pdf] Mathematical
Structures in Computer Science, 16(2):163-183, 2006
Bounded
functional
interpretation Fernando
Ferreira and Paulo Oliva
[pdf] Annals of Pure
and Applied Logic, 135:73-112, 2005
Modified
bar
recursion
and
classical
dependent
choice Ulrich Berger
and Paulo Oliva
[pdf] Lecture Notes
in Logic, 20:89-107, 2005
Proof
Mining
in
Subsystems
of
Analysis
Paulo Oliva
[pdf] PhD
dissertation, 198 pages, BRICS, Jul 2003
Polynomial-time
algorithms
from
ineffective
proofs
Paulo Oliva
[pdf] Proceedings of
LICS, 128-137, 2003
Proof
mining:
A
systematic
way
of
analyzing
proofs
in
mathematic Ulrich
Kohlenbach and Paulo Oliva
[pdf] Proc. Steklov
Inst. Math, 242:136-164, 2003
Proof
mining
in
L1 approximation Ulrich
Kohlenbach and Paulo Oliva
[pdf] Annals of Pure
and Applied Logic, 121:1-38, 2003
On
the computational complexity of L1-approximation
Paulo Oliva
[pdf] Mathematical
Logic Quarterly, 48(1):66-77, 2002
Reporting
exact
and
approximate
regular
expression
matches Kátia
Guimarães, E. W.
Myers and Paulo Oliva
[pdf] Proc. Ninth
Combinatorial Pattern Matching Conference,
Springer
LNCS 1448:91-103, 1998