Programming Systems Lab: Publications by Gert Smolka

Saarland University Computer Science

Select author:

2023

A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory   (pdf)
Yannick Forster, Felix Jahn, Gert Smolka
CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs

2021

A Mechanised Proof of the Time Invariance Thesis for the Weak Call-by-value λ-Calculus   (pdf)
Yannick Forster, Fabian Kunze, Gert Smolka, Maximilian Wuttke
12th International Conference on Interactive Theorem Proving (ITP 2021)

2020

A History of the Oz Multiparadigm Language   (pdf)
Peter Van Roy, Seif Haridi, Christian Schulte, Gert Smolka
Proceedings of the ACM on Programming Languages

2019

On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem   (pdf)
Yannick Forster, Dominik Kirst, Gert Smolka
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019

2018

Call-by-Value Lambda Calculus as a Model of Computation in Coq   (pdf)
Yannick Forster, Gert Smolka
Journal of Automated Reasoning

Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory   (pdf)
Dominik Kirst, Gert Smolka
Journal of Automated Reasoning

Formal Small-step Verification of a Call-by-value Lambda Calculus Machine   (pdf)
Fabian Kunze, Gert Smolka, Yannick Forster
16th Asian Symposium on Programming Languages and Systems, APLAS 2018, Wellington, New Zealand, December 2-6

Constructive Analysis of S1S and Büchi Automata   (pdf)
Moritz Lichter, Gert Smolka
arXiv:1804.04967

Large Model Constructions for Second-Order ZF in Dependent Type Theory   (pdf)
Dominik Kirst, Gert Smolka
Certified Programs and Proofs - 7th International Conference, CPP 2018, Los Angeles, USA, January 8-9, 2018

Verification of PCP-Related Computational Reductions in Coq   (pdf)
Yannick Forster, Edith Heiter, Gert Smolka
Interactive Theorem Proving - 9th International Conference, ITP 2018, Oxford, UK, July 9-12, 2018

Regular Language Representations in the Constructive Type Theory of Coq   (pdf)
Christian Doczkal, Gert Smolka
Journal of Automated Reasoning

2017

Relating System F and λ2: A Case Study in Coq, Abella and Beluga   (pdf)
Jonas Kaiser, Brigitte Pientka, Gert Smolka
Proceedings of FSCD 2017

Tower Induction and Up-To Techniques for CCS with Fixed Points   (pdf)
Steven Schäfer, Gert Smolka
Relational and Algebraic Methods in Computer Science: 16th International Conference, RAMiCS 2017, Lyon, France, May 15-18, 2017, Proceedings

Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq   (pdf)
Yannick Forster, Gert Smolka
Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017

Categoricity Results for Second-Order ZF in Dependent Type Theory   (pdf)
Dominik Kirst, Gert Smolka
Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017

Equivalence of System F and λ2 in Abella   (pdf)
Jonas Kaiser, Gert Smolka
Workshop Presentation at TTT 2017, Paris

Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas   (pdf)
Jonas Kaiser, Tobias Tebbi, Gert Smolka
Proceedings of CPP 2017

2016

An Inductive Proof Method for Simulation-based Compiler Correctness
Sigurd Schneider, Gert Smolka, Sebastian Hack
Technical Report

Hereditarily Finite Sets in Constructive Type Theory   (pdf)
Gert Smolka, Kathrin Stark
Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-27, 2016

Two-Way Automata in Coq   (pdf)
Christian Doczkal, Gert Smolka
Interactive Theorem Proving (ITP 2016)

Axiomatic Semantics for Compiler Verification   (pdf)
Steven Schäfer, Sigurd Schneider, Gert Smolka
5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, St. Petersburg, FL, USA, January 20-22

Completeness and Decidability Results for CTL in Constructive Type Theory   (pdf)
Christian Doczkal, Gert Smolka
Journal of Automated Reasoning

2015

Transfinite Constructions in Classical Type Theory   (pdf)
Gert Smolka, Steven Schäfer, Christian Doczkal
Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015

Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions   (pdf)
Steven Schäfer, Tobias Tebbi, Gert Smolka
Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015

A Linear First-Order Functional Intermediate Language for Verified Compilers   (pdf)
Sigurd Schneider, Gert Smolka, Sebastian Hack
Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015

Completeness and Decidability of de Bruijn Substitution Algebra in Coq   (pdf)
Steven Schäfer, Gert Smolka, Tobias Tebbi
Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015

2014

Completeness and Decidability Results for CTL in Coq   (pdf)
Christian Doczkal, Gert Smolka
Interactive Theorem Proving (ITP 2014)

A Goal-Directed Decision Procedure for Hybrid PDL   (pdf)
Mark Kaminski, Gert Smolka
Journal of Automated Reasoning

2013

Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification   (pdf)
Gert Smolka, Tobias Tebbi
24rd International Conference on Rewriting Techniques and Applications (RTA'13)

A Constructive Theory of Regular Languages in Coq   (pdf)
Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka
Certified Programs and Proofs, Third International Conference (CPP 2013)

2012

Constructive Completeness for Modal Logic with Transitive Closure   (pdf)
Christian Doczkal, Gert Smolka
Certified Programs and Proofs, Second International Conference (CPP 2012)

2011

Clausal Tableaux for Hybrid PDL   (pdf)
Mark Kaminski, Gert Smolka
M4M-7

Constructive Formalization of Hybrid Logic with Eventualities   (pdf)
Christian Doczkal, Gert Smolka
Certified Programs and Proofs, First International Conference (CPP 2011)

Correctness of an Incremental and Worst-Case Optimal Decision Procedure for Modal Logic with Eventualities   (pdf)
Mark Kaminski, Gert Smolka
Technical Report

Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics   (pdf)
Mark Kaminski, Thomas Schneider, Gert Smolka
TABLEAUX 2011

Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies
Mark Kaminski, Sigurd Schneider, Gert Smolka
Logical Methods in Computer Science

2010

Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference   (pdf)
Mark Kaminski, Gert Smolka
LPAR-17

Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles   (pdf)
Mark Kaminski, Gert Smolka
TCS 2010

Clausal Tableaux for Hybrid PDL   (pdf)
Mark Kaminski, Gert Smolka
Technical Report

Terminating Tableaux for Hybrid Logic with Eventualities   (pdf)
Mark Kaminski, Gert Smolka
IJCAR 2010

Analytic Tableaux for Simple Type Theory and its First-Order Fragment
Chad E. Brown, Gert Smolka
Logical Methods in Computer Science

Spartacus: A Tableau Prover for Hybrid Logic   (pdf)
Daniel Götzmann, Mark Kaminski, Gert Smolka
M4M-6

2009

Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles   (pdf)
Mark Kaminski, Gert Smolka
DL 2009

Complete Cut-Free Tableaux for Equational Simple Type Theory   (pdf)
Chad E. Brown, Gert Smolka
Technical Report

Extended First-Order Logic   (pdf)
Chad E. Brown, Gert Smolka
Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Proceedings

Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies   (pdf)
Mark Kaminski, Sigurd Schneider, Gert Smolka
TABLEAUX 2009

Terminating Tableau Systems for Hybrid Logic with Difference and Converse   (pdf)
Mark Kaminski, Gert Smolka
Journal of Logic, Language and Information

Terminating Tableaux for the Basic Fragment of Simple Type Theory   (pdf)
Chad E. Brown, Gert Smolka
TABLEAUX 2009

Hybrid Tableaux for the Difference Modality   (pdf)
Mark Kaminski, Gert Smolka
M4M-5

2008

A Minimal Propositional Type Theory   (pdf)
Mark Kaminski, Gert Smolka
Technical Report

A Finite Axiomatization of Propositional Type Theory in Pure Lambda Calculus   (pdf)
Mark Kaminski, Gert Smolka
Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday

Terminating Tableau Systems for Modal Logic with Equality   (pdf)
Mark Kaminski, Gert Smolka
Technical Report, Submitted

Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse   (pdf)
Mark Kaminski, Gert Smolka
IJCAR 2008

2007

A Straightforward Saturation-Based Decision Procedure for Hybrid Logic   (pdf)
Mark Kaminski, Gert Smolka
International Workshop on Hybrid Logic 2007 (HyLo 2007)

Higher-Order Syntax and Saturation Algorithms for Hybrid Logic   (pdf)
Moritz Hardt, Gert Smolka
Electronic Notes in Theoretical Computer Science

2006

Generating Propagators for Finite Set Constraints   (pdf)
Guido Tack, Christian Schulte, Gert Smolka
12th International Conference on Principles and Practice of Constraint Programming

Multi-dimensional Dependency Grammar as Multigraph Description   (pdf)
Ralph Debusmann, Gert Smolka
Proceedings of FLAIRS-19

A Concurrent Lambda Calculus with Futures   (pdf)
Joachim Niehren, Jan Schwinghammer, Gert Smolka
Theoretical Computer Science

Generic Pickling and Minimization   (pdf)
Guido Tack, Leif Kornstaedt, Gert Smolka
Proceedings of the ACM-SIGPLAN Workshop on ML (ML 2005)

Alice Through the Looking Glass   (pdf)
Andreas Rossberg, Didier Le Botlan, Guido Tack, Thorsten Brunklaus, Gert Smolka
Trends in Functional Programming, Volume 5

2005

Alice Through the Looking Glass (Extended Mix)   (pdf)
Andreas Rossberg, Didier Le Botlan, Guido Tack, Thorsten Brunklaus, Gert Smolka
Technical Report, Draft, \urlhttp://www.ps.uni-sb.de/Papers/

A Concurrent Lambda Calculus with Futures   (pdf)
Joachim Niehren, Jan Schwinghammer, Gert Smolka
5th International Workshop on Frontiers in Combining Systems

2004

A Relational Syntax-Semantics Interface Based on Dependency Grammar   (pdf)
Ralph Debusmann, Denys Duchier, Alexander Koller, Marco Kuhlmann, Gert Smolka, Stefan Thater
Proceedings of the 20th International Conference on Computational Linguistics (COLING 2004)

1999

Efficient Logic Variables for Distributed Computing   (pdf)
Seif Haridi, Peter Van Roy, Per Brand, Michael Mehl, Ralf Scheidhauer, Gert Smolka
ACM Transactions on Programming Languages and Systems

1998

Concurrent Constraint Programming Based on Functional Programming   (pdf)
Gert Smolka
Programming Languages and Systems

Futures and By-need Synchronization   (pdf)
Michael Mehl, Christian Schulte, Gert Smolka
Technical Report, DRAFT

A Higher-order Module Discipline with Separate Compilation, Dynamic Linking, and Pickling   (pdf)
Denys Duchier, Leif Kornstaedt, Christian Schulte, Gert Smolka
Technical Report, DRAFT

1997

An Overview of the Design of Distributed Oz   (pdf)
Seif Haridi, Peter Van Roy, Gert Smolka
Proceedings of the Second International Symposium on Parallel Symbolic Computation (PASCO '97)

Mobile Objects in Distributed Oz   (pdf)
Peter Van Roy, Seif Haridi, Per Brand, Gert Smolka, Michael Mehl, Ralf Scheidhauer
ACM Transactions on Programming Languages and Systems

1996

Oz: Nebenläufige Programmierung mit Constraints   (pdf)
Martin Müller, Gert Smolka
KI - Künstliche Intelligenz

Problem Solving with Constraints and Programming   (pdf)
Gert Smolka
ACM Computing Surveys

1995

The Oz Programming Model   (pdf)
Gert Smolka
Computer Science Today

Operational Semantics of Constraint Logic Programs with Coroutining   (pdf)
Andreas Podelski, Gert Smolka
Proceedings of the 1995 International Conference on Logic Programming

Object-Oriented Concurrent Constraint Programming in Oz   (pdf)
Gert Smolka, Martin Henz, Jörg Würtz
Principles and Practice of Constraint Programming

The Definition of Kernel Oz   (pdf)
Gert Smolka
Constraints: Basics and Trends

A Complete and Recursive Feature Theory   (pdf)
Rolf Backofen, Gert Smolka
Theoretical Computer Science

Situated Simplification   (pdf)
Andreas Podelski, Gert Smolka
Proceedings of the 1st Conference on Principles and Practice of Constraint Programming

1994

A Foundation for Higher-order Concurrent Constraint Programming   (pdf)
Gert Smolka
1st International Conference on Constraints in Computational Logics

Encapsulated Search in Higher-order Concurrent Constraint Programming   (pdf)
Christian Schulte, Gert Smolka
Logic Programming: Proceedings of the 1994 International Symposium

Encapsulated Search and Constraint Programming in Oz   (pdf)
Christian Schulte, Gert Smolka, Jörg Würtz
Second Workshop on Principles and Practice of Constraint Programming

A Calculus for Higher-Order Concurrent Constraint Programming with Deep Guards   (pdf)
Gert Smolka
Technical Report

A Confluent Relational Calculus for Higher-Order Programming with Constraints   (pdf)
Joachim Niehren, Gert Smolka
1st International Conference on Constraints in Computational Logics

Records for Logic Programming   (pdf)
Gert Smolka, Ralf Treinen
Journal of Logic Programming

A Feature-based Constraint System for Logic Programming with Entailment   (pdf)
Hassan Aït-Kaci, Andreas Podelski, Gert Smolka
Theoretical Computer Science

1993

Residuation and Guarded Rules for Constraint Logic Programming   (pdf)
Gert Smolka
Constraint Logic Programming: Selected Research

On the Expressivity of Feature Logics with Negation, Functional Uncertainty, and Sort Equations   (pdf)
Franz Baader, Hans-Jürgen Bürckert, Bernhard Nebel, Werner Nutt, Gert Smolka
Journal of Logic, Language and Information

Oz---A Programming Language for Multi-Agent Systems   (pdf)
Martin Henz, Gert Smolka, Jörg Würtz
13th International Joint Conference on Artificial Intelligence

1992

Feature Constraint Logics for Unification Grammars   (pdf)
Gert Smolka
Journal of Logic Programming

1991

Attributive concept descriptions with complements   (pdf)
Manfred Schmidt-Schauß, Gert Smolka
Artificial Intelligence

Attributive Description Formalisms and the Rest of the World   (pdf)
Bernhard Nebel, Gert Smolka
Text Understanding in LILOG

1990

Representation and Reasoning with Attributive Descriptions   (pdf)
Bernhard Nebel, Gert Smolka
Sorts and Types in Artificial Intelligence

1989

Logic Programming over Polymorphically Order-Sorted Types   (pdf)
Gert Smolka
PhD Thesis, Fachbereich Informatik,Universität Kaiserslautern

1988

TEL (Version 0.9), Report and User Manual   (pdf)
Gert Smolka
Technical Report

Definite Relations over Constraint Languages   (pdf)
Markus Höhfeld, Gert Smolka
Technical Report

A Feature Logic with Subsorts   (pdf)
Gert Smolka
Technical Report, To appear in: J. Wedekind and C. Rohrer (eds.), Unification in Grammar; The MIT Press, 1991


Login to edit


Legal notice, Privacy policy