Publications of Wojciech Moczydlowski

• Wojciech Moczydlowski Bridging the Gap Between Replacement and Collection by Inaccessible Sets. Invited talk at Special Session on Constructive Mathematics at 2009 AMS Fall Southeastern Meeting. Abstract published in AMS Meeting # 1053, Notices.
  

• Wojciech Moczydlowski Unifying Sets and Programs via Dependent Types. Proceedings of Symposium on Logical Foundations of Computer Science (LFCS 2009), 365-379, Springer. Invited to the special issue of Annals of Pure and Applied Logic.
  

• Wojciech Moczydlowski Investigations on Sets and Types. Ph. D. Thesis. Cornell University. Awarded the 2007 Sacks Prize. Nominated to ACM Doctoral Dissertation Award.
  [ps] [pdf]

• Wojciech Moczydlowski A Dependent Set Theory. Proceedings of 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 23-34, IEEE Computer Society.
  [ps] [pdf] [IEEE authoritative version] [BiBTeX]

• Robert Constable and Wojciech Moczydlowski Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus. Proceedings of Symposium on Logical Foundations of Computer Science (LFCS 2007), LNCS 4514, 147-161, Springer. Invited to the special issue of Annals of Pure and Applied Logic.
  [ps] [pdf] [SpringerLink] [BiBTeX]
  
  A previous version is available as:
  • Robert Constable and Wojciech Moczydlowski Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus. Cornell University Technical Report 2006-2061.
    [ps] [pdf]

• Wojciech Moczydlowski A Normalizing Intuitionistic Set Theory with Inaccessible Sets. Logical Methods in Computer Science, volume 3 (3:6) 2007, pages 1-31.
  [ps][pdf]
  
  A previous version is available as:
  • Wojciech Moczydlowski A Normalizing Intuitionistic Set Theory with Inaccessible Sets. Cornell University Technical Report 2006-2051.
    [ps] [pdf]

• Wojciech Moczydlowski Normalization of intuitionistic set theories. Proceedings of Eighth International Workshop on Termination (WST 2006), 27-31. To appear in CoRR.
  [ps] [pdf]
  

• Robert Constable and Wojciech Moczydlowski Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics. Proceedings of 3rd International Joint Conference on Automated Reasoning (IJCAR 2006), LNCS 4130, 162-176, Springer. Invited to the special issue of Logical Methods in Computer Science.
  [ps] [pdf] [SpringerLink] [BiBTeX]

• Wojciech Moczydlowski Normalization of IZF with Replacement. Proceedings of 15th Annual Conference of European Association for Computer Science Logic (CSL 2006), LNCS 4207, 516-530, Springer. Invited to the special issue of Logical Methods in Computer Science.
  [ps] [pdf] [SpringerLink] [BiBTeX]
  
  A longer version is available as:
  • Wojciech Moczydlowski Normalization of IZF with Replacement. Cornell University Technical Report 2006-2024.
    [ps] [pdf]

• Wojciech Moczydlowski and Alfons Geser Termination of Single-Threaded One-rule Semi-Thue Systems. Proceedings of 16th International Conference on Rewriting Techniques and Applications (RTA 2005), LNCS 3467, 338-352, Springer.
  [ps] [pdf] [SpringerLink] [BiBTeX]
  
  A previous version is available as:
  • Wojciech Moczydlowski and Alfons Geser Termination of Single-Threaded One-rule Semi-Thue Systems. Tech. Rep. U. Warsaw 273, 2002.
    [ps]

• Wojciech Moczydlowski Model-theoretic proofs of Gödel's Second Theorem. M. S. thesis in the field of mathematics (in Polish).
  [ps]

• Wojciech Moczydlowski One-rule string rewriting systems. M. S. thesis in the field of computer science (in Polish).
  [ps]