Paul J. Voda

Research Interests:
-
theory and practice of declarative programming languages,
-
mathematical logic, theory of computability, Peano arithmetic.
Main Project:
Some Papers:
-
Pair Based Subrecursion,
Habilitatitionschrift, 1994, (.ps.gz: 135K)
-
Subrecursion
as Basis for a Feasible Programming language , Conf. Computer Science Logic,
September 94, Lecture Notes in Computer Science 933, Springer Verlag
1995, (.ps.gz: 75K)
-
Programming by
Logic and Logic by Programming , with J.
Komara invited talk at SOFSEM '94, Czech Republic 1994, (.ps.gz: 142K)
-
Syntactic Reduction
of Predicate Tableaux to Propositional Tableauxwith J.
Komara Workshop on Theorem Proving and Analytic Tableaux, May 1995,
Lecture Notes in Artificial Intelligence vol 918, Springer Verlag 1995,
(.ps.gz: 70K)
-
On Herbrand
Skeletons with J. Komara
,
TR102 Institute of Informatics, July 1995, (.ps.gz 77K)
-
On Quasitautologies
with
J.
Komara , Intern. Conference Tableaux'97 Pont a Mousson, May 1997, Lecture
Notes in Artificial Intelligence vol 1227, Springer Verlag 1997, (.ps.gz:
54K)
-
A Simple Ordinal
Recursive Normalization of Goedel's T, Conf. Computer Science Logic;
Aarhus, August 1997, Lecture Notes in Computer Science vol 1414, Springer
Verlag 1998 (.ps.gz 61K)
-
Computer Programming
as Mathematics , with J.
Komara tutorial in Intern. Conference Tableaux'98, May 1998, Lecture
Notes in Artificial Intelligence vol 1397, Springer Verlag 1998 (.ps.gz:
31K)
-
Theorems of Peter
and Parsons in Computer Programming, with J.
Komara , Conf. Computer Science Logic; Brno, August 1998, Lecture
Notes in Computer Science vol 1584, Springer Verlag 1999,
-
A Note on the Exponential
Relation in Peano Arithmetic
, December
1998, see a simplified version below,
-
Extraction of Efficient Programs in Sigma1 Arithmetic
, with J.
Komara
, January 2000,
-
Two Simple Intrinsic Characterizations of Main Complexity Classes
, October 2001,
-
A Note on the Exponential
Relation in Peano Arithmetic II
, November
2001,
-
Recursion and Coding in PA
by Techniques of Computer Programming
, December
2001,
-
An Exercise in Programming
in PA: Fast Growing Hierarchy Functions
, February
2002,
-
Predicative Justification and Development of a Second Order Theory of Finite Sets
, January 2003,
-
What Can we Gain by Integrating a Language Processor
with a Theorem Prover?
, February 2003,
-
Grundlagenstreit in the Theory of Programming , February 2003,
-
From Declarative to Imperative Proof-Carrying Programs with Jan Kluka, July 2003.
-
The Surprising Power of Restricted Programs and Goedel's Functionals
, with
Lars Kristiansen, Conf. Computer Science Logic;
Vienna August 2003, Lecture
Notes in Computer Science vol 2803, Springer Verlag 2003,
-
Complexity Classes and Fragments of C ,
with
Lars Kristiansen,
Information Processing Letters, Vol 88/5 pp 213-218, October 2003,
-
Programming Languages Capturing Complexity Classes ,
with
Lars Kristiansen,
NWPT-04 Uppsala October 2004,
-
Forcing in DPLL Satisfiability Solving with Jan Kluka, February 2005.
-
Kleene-Kreisel Functionals and Computational Complexity,
with
Lars Kristiansen,
Cie 2005: New Computational Paradigms. Cooper, Loewe, Leen, Torenvliet (eds.) X-2005-01
ILLC Scientific Publications, Technical Notes Series, Institute for Logic, Language and Computation, University of Amsterdam, pp. 225-226.
-
Programming languages capturing complexity classes, with
Lars Kristiansen,
Nordic Journal of Computing 12 (2005), 89-115.
-
The Trade-off theorem and fragments of and Goedel's T,
with
Lars Kristiansen,
Jin-Yi Cai, S. Barry Cooper and Angsheng Li (eds.),
TAMC'06: Theory and Applications of Models of Computation, LNCS 3959, pp. 654-674, Springer-Verlag 2006.
-
Constant Detours do not Matter, with Lars Kristiansen, November 2006.
-
Nondeterminism without Turing Machines,
with
M. Barra and Lars Kristiansen,
in the local proceedings CiE 2007.
-
The Structure of Detour Degrees,
with
Lars Kristiansen,
Theory and Applications of Models of Computation, 5th International Conference, TAMC 2008, Xi'an, China, April 25-29, 2008. Proceedings. Lecture Notes in Computer Science 4978 Springer 2008.
-
A Simple and Practical Valuation Tree Calculus for First-Order Logic.
with
Jan Kluka,
CiE 2009.
-
A Proof Calculus with Case Analysis as its Only Rule
with
Jan Kluka,
Submitted to CSL 2009.
Lecture Notes and Texts:
-
Peano Arithmetic and Clausal Language,
Lecture notes used in the course Logic for Computer Scientists describing in
detail the bootstrapping of
Peano Arithmetic up to and including the introduction of recursive definitions of CL.
Dated: November 2004.
-
Theory of Recursive
Functions & Computability (from Computer Programmer's View),
(.ps.gz 380K). Text on computability theory with a large chapter
on CL (175 pages).
Dated: March 2000.
Contents:
Introduction
-
Overview of CL
-
Recursive Functions
-
Inductively defined Function Classes
-
Primitive Recursive Functions
-
Characterization of Recursive Functions
-
Computability
-
Beyond Computability
-
Meta-Mathematics
of Computer Programming ,
(.ps.gz 685K). Draft of a monograph on the theory of computer
programming (cca 300 pages)
Dated: May 2001.
Contents:
-
Why the Theory of Programming in Peano Arithmetic? (extended introduction
see next item)
-
First-Order Languages
-
Propositional Logic
-
Identity Logic
-
Quantification Logic
-
First-Order Theories
-
Peano Arithmetic (PA)
-
Recursive Bootstrapping of PA
-
Proof Theory of PA (not yet done)
-
Clausal Language (not yet done)
-
Computation of Clausal Programs (not yet done)
-
Data Types (not yet done)
-
Functional Programming (not yet done)
-
Modular Programming (not yet done)
-
Meta-Mathematics
of Computer Programming (only introduction),
(.ps.gz 266K). Contains the table of contents, preface,
chapter Why the Theory of Programming in Peano Arithmetic?, and
references of the above monograph (cca 100 pages).
Dated: May 2001.
Contents:
-
Effectively Computable Functions
-
Imperative vs. Declarative Programming
-
Arguments in Favor of Natural Numbers
-
Bootstrapping of PA
-
Clausal Extensions of PA
-
Limits of Provably Recursive Definitions in PA
-
Computation of Clausal Definitions
-
Data Types
-
Intensional Funtionals
-
Second-Order Issues of Modularity (not yet done)
-
Issues Open to Further Research (not yet done)
-
Programming by Logic
& Logic by Programming
,
(.ps.gz 526). Older version of the text on computability (263
pages).
Dated: May, 1996.
Contents:
Introduction
-
Domain of Computability
-
Computability
-
Language Characterization of Computable Functions
-
Primitive Pair Recursive Functions
-
Pair Computability versus Classical Computability
-
Beyond Computability
-
Fine Structure of Primitive Pair recursive Functions
Paul J. Voda
Institute of Informatics,
Faculty of Math. Phys. and Informatics, Comenius University
Mlynska Dolina,
84215 Bratislava
SLOVAKIA
email: voda at fmph dot uniba dot sk
Last updated: March 2005