Paul J. Voda 

Research Interests:

• theory and practice of declarative programming languages,
• mathematical logic, theory of computability, Peano arithmetic.

Main Project:

• CL (Clausal Language), a declarative programming language and proof system

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

1. Overview of CL
2. Recursive Functions
3. Inductively defined Function Classes
4. Primitive Recursive Functions
5. Characterization of Recursive Functions
6. Computability
7. 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:
 

1. Why the Theory of Programming in Peano Arithmetic? (extended introduction see next item)
2. First-Order Languages
3. Propositional Logic
4. Identity Logic
5. Quantification Logic
6. First-Order Theories
7. Peano Arithmetic (PA)
8. Recursive Bootstrapping of PA
9. Proof Theory of PA (not yet done)
10. Clausal Language (not yet done)
11. Computation of Clausal Programs (not yet done)
12. Data Types (not yet done)
13. Functional Programming (not yet done)
14. 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:

1.  Effectively Computable Functions
2. Imperative vs. Declarative Programming
3. Arguments in Favor of Natural Numbers
4. Bootstrapping of PA
5. Clausal Extensions of PA
6. Limits of Provably Recursive Definitions in PA
7. Computation of Clausal Definitions
8. Data Types
9. Intensional Funtionals
10. Second-Order Issues of Modularity (not yet done)
11. 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

1. Domain of Computability
2. Computability
3. Language Characterization of Computable Functions
4. Primitive Pair Recursive Functions
5. Pair Computability versus Classical Computability
6. Beyond Computability
7. Fine Structure of Primitive Pair recursive Functions