Gert Smolka

Publication Activity (10 Years)

Years Active: 1980-2023
Publications (10 Years): 28

Top Venues

ITP

CPP

CoRR

J. Autom. Reason.

Kaiserslautern University of Technology, Germany (PHD)

Education History

Kaiserslautern University of Technology, Germany

PHD

Publications

Yannick Forster, Felix Jahn, Gert Smolka
A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). CPP (2023)
Yannick Forster, Fabian Kunze, Gert Smolka, Maximilian Wuttke
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. ITP (2021)
Peter Van Roy, Seif Haridi, Christian Schulte, Gert Smolka
A history of the Oz multiparadigm language. Proc. ACM Program. Lang. 4 (HOPL) (2020)
Dominik Kirst, Gert Smolka
Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory. J. Autom. Reason. 63 (2) (2019)
Yannick Forster, Dominik Kirst, Gert Smolka
On synthetic undecidability in coq, with an application to the entscheidungsproblem. CPP (2019)
Yannick Forster, Gert Smolka
Call-by-Value Lambda Calculus as a Model of Computation in Coq. J. Autom. Reason. 63 (2) (2019)
Moritz Lichter, Gert Smolka
Constructive Analysis of S1S and Büchi Automata. CoRR (2018)
Fabian Kunze, Gert Smolka, Yannick Forster
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine. CoRR (2018)
Yannick Forster, Edith Heiter, Gert Smolka
Verification of PCP-Related Computational Reductions in Coq. ITP (2018)
Dominik Kirst, Gert Smolka
Large model constructions for second-order ZF in dependent type theory. CPP (2018)
Fabian Kunze, Gert Smolka, Yannick Forster
Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine. APLAS (2018)
Christian Doczkal, Gert Smolka
Regular Language Representations in the Constructive Type Theory of Coq. J. Autom. Reason. 61 (1-4) (2018)
Jonas Kaiser, Tobias Tebbi, Gert Smolka
Equivalence of system f and ź2 in Coq based on context morphism lemmas. CPP (2017)
Jonas Kaiser, Brigitte Pientka, Gert Smolka
Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. FSCD (2017)
Yannick Forster, Gert Smolka
Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. ITP (2017)
Yannick Forster, Edith Heiter, Gert Smolka
Verification of PCP-Related Computational Reductions in Coq. CoRR (2017)
Dominik Kirst, Gert Smolka
Categoricity Results for Second-Order ZF in Dependent Type Theory. ITP (2017)
Steven Schäfer, Gert Smolka
Tower Induction and Up-to Techniques for CCS with Fixed Points. RAMiCS (2017)
Christian Doczkal, Gert Smolka
Two-Way Automata in Coq. ITP (2016)
Steven Schäfer, Sigurd Schneider, Gert Smolka
Axiomatic semantics for compiler verification. CPP (2016)
Gert Smolka, Kathrin Stark
Hereditarily Finite Sets in Constructive Type Theory. ITP (2016)
Sigurd Schneider, Gert Smolka, Sebastian Hack
An Inductive Proof Method for Simulation-based Compiler Correctness. CoRR (2016)
Christian Doczkal, Gert Smolka
Completeness and Decidability Results for CTL in Constructive Type Theory. J. Autom. Reason. 56 (3) (2016)
Sigurd Schneider, Gert Smolka, Sebastian Hack
A Linear First-Order Functional Intermediate Language for Verified Compilers. ITP (2015)
Gert Smolka, Steven Schäfer, Christian Doczkal
Transfinite Constructions in Classical Type Theory. ITP (2015)
Steven Schäfer, Tobias Tebbi, Gert Smolka
Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. ITP (2015)
Sigurd Schneider, Gert Smolka, Sebastian Hack
A First-Order Functional Intermediate Language for Verified Compilers. CoRR (2015)
Steven Schäfer, Gert Smolka, Tobias Tebbi
Completeness and Decidability of de Bruijn Substitution Algebra in Coq. CPP (2015)
Mark Kaminski, Gert Smolka
A Goal-Directed Decision Procedure for Hybrid PDL. J. Autom. Reason. 52 (4) (2014)
Christian Doczkal, Gert Smolka
Completeness and Decidability Results for CTL in Coq. ITP (2014)
Gert Smolka, Tobias Tebbi
Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification. RTA (2013)
Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka
A Constructive Theory of Regular Languages in Coq. CPP (2013)
Mark Kaminski, Gert Smolka
Correctness of an Incremental and Worst-Case Optimal Decision Procedure for Modal Logic with Eventualities CoRR (2012)
Christian Doczkal, Gert Smolka
Constructive Completeness for Modal Logic with Transitive Closure. CPP (2012)
Mark Kaminski, Thomas Schneider, Gert Smolka
Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics. TABLEAUX (2011)
Christian Doczkal, Gert Smolka
Constructive Formalization of Hybrid Logic with Eventualities. CPP (2011)
Mark Kaminski, Sigurd Schneider, Gert Smolka
Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies Log. Methods Comput. Sci. 7 (1) (2011)
Gert Smolka
Incremental Decision Procedures for Modal Logic with Nominals and Eventualities. Description Logics (2011)
Mark Kaminski, Gert Smolka
Clausal Tableaux for Hybrid PDL. Electron. Notes Theor. Comput. Sci. 278 (2011)
Mark Kaminski, Gert Smolka
\mathcal{SOQ} with Number Restrictions on Transitive Roles. IFIP TCS (2010)
Mark Kaminski, Gert Smolka
Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference. LPAR (Yogyakarta) (2010)
Daniel Götzmann, Mark Kaminski, Gert Smolka
Spartacus: A Tableau Prover for Hybrid Logic. Electron. Notes Theor. Comput. Sci. 262 (2010)
Chad E. Brown, Gert Smolka
Analytic Tableaux for Simple Type Theory and its First-Order Fragment Log. Methods Comput. Sci. 6 (2) (2010)
Mark Kaminski, Gert Smolka
A Minimal Propositional Type Theory CoRR (2010)
Mark Kaminski, Gert Smolka
Terminating Tableaux for Hybrid Logic with Eventualities. IJCAR (2010)
Chad E. Brown, Gert Smolka
Terminating Tableaux for the Basic Fragment of Simple Type Theory. TABLEAUX (2009)
Mark Kaminski, Gert Smolka
Hybrid Tableaux for the Difference Modality. Electron. Notes Theor. Comput. Sci. 231 (2009)
Mark Kaminski, Gert Smolka
Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles. Description Logics (2009)
Mark Kaminski, Gert Smolka
Terminating Tableau Systems for Hybrid Logic with Difference and Converse. J. Log. Lang. Inf. 18 (4) (2009)
Chad E. Brown, Gert Smolka
Extended First-Order Logic. TPHOLs (2009)
Mark Kaminski, Sigurd Schneider, Gert Smolka
Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies. TABLEAUX (2009)
Mark Kaminski, Gert Smolka
Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse. IJCAR (2008)
Moritz Hardt, Gert Smolka
Higher-Order Syntax and Saturation Algorithms for Hybrid Logic. Electron. Notes Theor. Comput. Sci. 174 (6) (2007)
Joachim Niehren, Jan Schwinghammer, Gert Smolka
A concurrent lambda calculus with futures. Theor. Comput. Sci. 364 (3) (2006)
Guido Tack, Leif Kornstaedt, Gert Smolka
Generic Pickling and Minimization. Electron. Notes Theor. Comput. Sci. 148 (2) (2006)
Guido Tack, Christian Schulte, Gert Smolka
Generating Propagators for Finite Set Constraints. CP (2006)
Ralph Debusmann, Gert Smolka
Multi-Dimensional Dependency Grammar as Multigraph Description. FLAIRS Conference (2006)
Joachim Niehren, Jan Schwinghammer, Gert Smolka
A Concurrent Lambda Calculus with Futures. FroCoS (2005)
Gert Smolka
The Development of Oz and Mozart. MOZ (2004)
Ralph Debusmann, Denys Duchier, Alexander Koller, Marco Kuhlmann, Gert Smolka, Stefan Thater
A Relational Syntax-Semantics Interface Based on Dependency Grammar. COLING (2004)
Andreas Rossberg, Didier Le Botlan, Guido Tack, Thorsten Brunklaus, Gert Smolka
Alice through the looking glass. Trends in Functional Programming (2004)
Gert Smolka
Introduction. Constraints An Int. J. 5 (1/2) (2000)
Gert Smolka
Guest Editor's Foreword. Nord. J. Comput. 7 (4) (2000)
Seif Haridi, Peter Van Roy, Per Brand, Michael Mehl, Ralf Scheidhauer, Gert Smolka
Efficient logic variables for distributed computing. ACM Trans. Program. Lang. Syst. 21 (3) (1999)
Gert Smolka
Concurrent Constraint Programming Based on Functional Programming (Extended Abstract). ESOP (1998)
Peter Van Roy, Seif Haridi, Per Brand, Gert Smolka, Michael Mehl, Ralf Scheidhauer
Mobile Objects in Distributed Oz. ACM Trans. Program. Lang. Syst. 19 (5) (1997)
Andreas Podelski, Gert Smolka
Situated Simplification. Theor. Comput. Sci. 173 (1) (1997)
Seif Haridi, Peter Van Roy, Gert Smolka
An overview of the design of Distributed Oz. PASCO (1997)
Gert Smolka
Constraint Programming in Oz (Abstract). ILPS (1997)
Martin Müller, Gert Smolka
Oz: nebenläufige Programmierung mit Constraints. Künstliche Intell. 10 (3) (1996)
Gert Smolka
Constraints in OZ. ACM Comput. Surv. 28 (4es) (1996)
Gert Smolka
The Oz Programming Language and System (Abstract). ASIAN (1996)
Gert Smolka
The Oz Programming Model. JELIA (1996)
Gert Smolka
Objects in a higher-order concurrent constraint model with state. LMO (1995)
Rolf Backofen, Gert Smolka
A Complete and Recursive Feature Theory. Theor. Comput. Sci. 146 (1&2) (1995)
Andreas Podelski, Gert Smolka
Situated Simplification. ICLP (1995)
Gert Smolka
The Oz Programming Model (Extended Abstract). Euro-Par (1995)
Gert Smolka
Oz: Concurrent Constraint Programming for Real. ICLP (1995)
Andreas Podelski, Gert Smolka
Operational Semantics of Constraint Logic Programs with Coroutining. ICLP (1995)
Andreas Podelski, Gert Smolka
Situated Simplification. CP (1995)
Gert Smolka
The Definition of Kernel Oz Constraint Programming (1994)
Christian Schulte, Gert Smolka, Jörg Würtz
Encapsulated Search and Constraint Programming in Oz. PPCP (1994)
Christian Schulte, Gert Smolka
Encapsulated Search for Higher-order Concurrent Constraint Programming. ILPS (1994)
Hassan Aït-Kaci, Andreas Podelski, Gert Smolka
A Feature Constraint System for Logic Programming with Entailment. Theor. Comput. Sci. 122 (1&2) (1994)
Joachim Niehren, Gert Smolka
A Confluent Relational Calculus for Higher-Order Programming with Constraints. CCL (1994)
Gert Smolka, Ralf Treinen
Records for Logic Programming. J. Log. Program. 18 (3) (1994)
Rolf Backofen, Gert Smolka
A Complete and Recursive Feature Theory. CoRR (1994)
Andreas V. Hense, Gert Smolka
A Record Calculus with Principal Types. CCL (1994)
Gert Smolka
A Foundation for Higher-order Concurrent Constraint Programming. CCL (1994)
Franz Baader, Hans-Jürgen Bürckert, Bernhard Nebel, Werner Nutt, Gert Smolka
On the expressivity of feature logics with negation, functional uncertainty, and sort equations. J. Log. Lang. Inf. 2 (1) (1993)
Gert Smolka, Martin Henz, Jörg Würtz
Object-Oriented Concurrent Constraint Programming in Oz. KI (1993)
Gert Smolka
A Survey of Oz - A Higher-order Concurrent Constraint Language. ICLP Workshop on Concurrent Constraint Programming (1993)
Rolf Backofen, Gert Smolka
A Complete and Recursive Feature Theory. ACL (1993)
Martin Henz, Gert Smolka, Jörg Würtz
Oz - A Programming Language for Multi-Agent Systems. IJCAI (1993)
Gert Smolka
Nebenläfige Objekte und Logische Programmierung. WLP (1993)
Gert Smolka, Ralf Treinen
Records for Logic Programming. JICSLP (1992)
Hassan Aït-Kaci, Andreas Podelski, Gert Smolka
A Feature-Based Constraint System for Logic Programming with Entailment. FGCS (1992)
Andreas V. Hense, Gert Smolka
A Verification of Extensible Record Types. IWAR (1992)
Gert Smolka
Feature-Constraint Logics for Unification Grammars. J. Log. Program. 12 (1&2) (1992)
Bernhard Nebel, Gert Smolka
Attribute Description Formalisms ... and the Rest of the World. Text Understanding in LILOG (1991)

Gert Smolka.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Gert Smolka