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
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)
A History of the Oz Multiparadigm Language
(pdf)
Peter Van Roy, Seif Haridi, Christian Schulte, Gert Smolka
Proceedings of the ACM on Programming Languages
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
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
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
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
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
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
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)
Constructive Completeness for Modal Logic with Transitive Closure
(pdf)
Christian Doczkal, Gert Smolka
Certified Programs and Proofs, Second International Conference (CPP 2012)
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
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
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
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
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
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
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
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)
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
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
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
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
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
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
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
Feature Constraint Logics for Unification Grammars
(pdf)
Gert Smolka
Journal of Logic Programming
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
Representation and Reasoning with Attributive Descriptions
(pdf)
Bernhard Nebel, Gert Smolka
Sorts and Types in Artificial Intelligence
Logic Programming over Polymorphically Order-Sorted Types
(pdf)
Gert Smolka
PhD Thesis, Fachbereich Informatik,Universität Kaiserslautern
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