default search action
Gert Smolka
Person information
- affiliation: Saarland University, Saarbrücken, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2023
- [c83]Yannick Forster
, Felix Jahn, Gert Smolka:
A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). CPP 2023: 159-166 - 2021
- [c82]Yannick Forster
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. ITP 2021: 19:1-19:20 - 2020
- [j25]Peter Van Roy, Seif Haridi, Christian Schulte, Gert Smolka:
A history of the Oz multiparadigm language. Proc. ACM Program. Lang. 4(HOPL): 83:1-83:56 (2020)
2010 – 2019
- 2019
- [j24]Yannick Forster
Call-by-Value Lambda Calculus as a Model of Computation in Coq. J. Autom. Reason. 63(2): 393-413 (2019) - [j23]Dominik Kirst
Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory. J. Autom. Reason. 63(2): 415-438 (2019) - [c81]Yannick Forster
On synthetic undecidability in coq, with an application to the entscheidungsproblem. CPP 2019: 38-51 - 2018
- [j22]Christian Doczkal
Regular Language Representations in the Constructive Type Theory of Coq. J. Autom. Reason. 61(1-4): 521-553 (2018) - [c80]Fabian Kunze, Gert Smolka, Yannick Forster
Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine. APLAS 2018: 264-283 - [c79]Dominik Kirst, Gert Smolka:
Large model constructions for second-order ZF in dependent type theory. CPP 2018: 228-239 - [c78]Yannick Forster
Verification of PCP-Related Computational Reductions in Coq. ITP 2018: 253-269 - [i13]Moritz Lichter, Gert Smolka:
Constructive Analysis of S1S and Büchi Automata. CoRR abs/1804.04967 (2018) - [i12]Fabian Kunze, Gert Smolka, Yannick Forster
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine. CoRR abs/1806.03205 (2018) - 2017
- [c77]Steven Schäfer, Gert Smolka:
Tower Induction and Up-to Techniques for CCS with Fixed Points. RAMiCS 2017: 274-289 - [c76]Jonas Kaiser, Tobias Tebbi, Gert Smolka:
Equivalence of system f and ź2 in Coq based on context morphism lemmas. CPP 2017: 222-234 - [c75]Yannick Forster
Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. ITP 2017: 189-206 - [c74]Dominik Kirst, Gert Smolka:
Categoricity Results for Second-Order ZF in Dependent Type Theory. ITP 2017: 304-318 - [c73]Jonas Kaiser, Brigitte Pientka, Gert Smolka:
Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. FSCD 2017: 21:1-21:19 - [i11]Yannick Forster
Verification of PCP-Related Computational Reductions in Coq. CoRR abs/1711.07023 (2017) - 2016
- [j21]Christian Doczkal, Gert Smolka:
Completeness and Decidability Results for CTL in Constructive Type Theory. J. Autom. Reason. 56(3): 343-365 (2016) - [c72]Steven Schäfer, Sigurd Schneider, Gert Smolka:
Axiomatic semantics for compiler verification. CPP 2016: 188-196 - [c71]Christian Doczkal, Gert Smolka:
Two-Way Automata in Coq. ITP 2016: 151-166 - [c70]Gert Smolka, Kathrin Stark:
Hereditarily Finite Sets in Constructive Type Theory. ITP 2016: 374-390 - [i10]Sigurd Schneider, Gert Smolka, Sebastian Hack:
An Inductive Proof Method for Simulation-based Compiler Correctness. CoRR abs/1611.09606 (2016) - 2015
- [c69]Steven Schäfer, Gert Smolka, Tobias Tebbi:
Completeness and Decidability of de Bruijn Substitution Algebra in Coq. CPP 2015: 67-73 - [c68]Sigurd Schneider, Gert Smolka, Sebastian Hack:
A Linear First-Order Functional Intermediate Language for Verified Compilers. ITP 2015: 344-358 - [c67]Steven Schäfer, Tobias Tebbi, Gert Smolka:
Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. ITP 2015: 359-374 - [c66]Gert Smolka, Steven Schäfer, Christian Doczkal:
Transfinite Constructions in Classical Type Theory. ITP 2015: 391-404 - [i9]Sigurd Schneider, Gert Smolka, Sebastian Hack:
A First-Order Functional Intermediate Language for Verified Compilers. CoRR abs/1503.08665 (2015) - 2014
- [j20]Mark Kaminski, Gert Smolka:
A Goal-Directed Decision Procedure for Hybrid PDL. J. Autom. Reason. 52(4): 407-450 (2014) - [c65]Christian Doczkal, Gert Smolka:
Completeness and Decidability Results for CTL in Coq. ITP 2014: 226-241 - 2013
- [c64]Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka:
A Constructive Theory of Regular Languages in Coq. CPP 2013: 82-97 - [c63]Gert Smolka, Tobias Tebbi:
Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification. RTA 2013: 271-286 - 2012
- [c62]Christian Doczkal, Gert Smolka:
Constructive Completeness for Modal Logic with Transitive Closure. CPP 2012: 224-239 - [i8]Mark Kaminski, Gert Smolka:
Correctness of an Incremental and Worst-Case Optimal Decision Procedure for Modal Logic with Eventualities. CoRR abs/1209.1248 (2012) - 2011
- [j19]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) - [c61]Christian Doczkal, Gert Smolka:
Constructive Formalization of Hybrid Logic with Eventualities. CPP 2011: 5-20 - [c60]Gert Smolka:
Incremental Decision Procedures for Modal Logic with Nominals and Eventualities. Description Logics 2011 - [c59]Mark Kaminski, Thomas Schneider, Gert Smolka:
Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics. TABLEAUX 2011: 196-210 - [c58]Mark Kaminski, Gert Smolka:
Clausal Tableaux for Hybrid PDL. M4M/LAMAS 2011: 99-113 - 2010
- [j18]Chad E. Brown, Gert Smolka:
Analytic Tableaux for Simple Type Theory and its First-Order Fragment. Log. Methods Comput. Sci. 6(2) (2010) - [c57]Mark Kaminski, Gert Smolka:
Terminating Tableaux for Hybrid Logic with Eventualities. IJCAR 2010: 240-254 - [c56]Mark Kaminski, Gert Smolka:
Terminating Tableaux for SOQ\mathcal{SOQ} with Number Restrictions on Transitive Roles. IFIP TCS 2010: 213-228 - [c55]Mark Kaminski, Gert Smolka:
Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference. LPAR (Yogyakarta) 2010: 417-431 - [i7]Mark Kaminski, Gert Smolka:
A Minimal Propositional Type Theory. CoRR abs/1001.4021 (2010)
2000 – 2009
- 2009
- [j17]Mark Kaminski, Gert Smolka:
Terminating Tableau Systems for Hybrid Logic with Difference and Converse. J. Log. Lang. Inf. 18(4): 437-464 (2009) - [c54]Mark Kaminski, Gert Smolka:
Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles. Description Logics 2009 - [c53]Chad E. Brown, Gert Smolka:
Terminating Tableaux for the Basic Fragment of Simple Type Theory. TABLEAUX 2009: 138-151 - [c52]Mark Kaminski, Sigurd Schneider, Gert Smolka:
Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies. TABLEAUX 2009: 235-249 - [c51]Chad E. Brown, Gert Smolka:
Extended First-Order Logic. TPHOLs 2009: 164-179 - [c50]Daniel Götzmann, Mark Kaminski, Gert Smolka:
Spartacus: A Tableau Prover for Hybrid Logic. M4M 2009: 127-139 - 2008
- [b2]Gert Smolka:
Programmierung - eine Einführung in die Informatik mit Standard ML. Oldenbourg 2008, ISBN 978-3-486-58601-5, pp. I-XIV, 1-371 - [c49]Mark Kaminski, Gert Smolka:
Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse. IJCAR 2008: 210-225 - 2007
- [c48]Mark Kaminski, Gert Smolka:
Hybrid Tableaux for the Difference Modality. M4M 2007: 241-257 - 2006
- [j16]Joachim Niehren, Jan Schwinghammer, Gert Smolka:
A concurrent lambda calculus with futures. Theor. Comput. Sci. 364(3): 338-356 (2006) - [c47]Guido Tack, Christian Schulte, Gert Smolka:
Generating Propagators for Finite Set Constraints. CP 2006: 575-589 - [c46]Ralph Debusmann, Gert Smolka:
Multi-Dimensional Dependency Grammar as Multigraph Description. FLAIRS 2006: 740-745 - [c45]Moritz Hardt, Gert Smolka:
Higher-Order Syntax and Saturation Algorithms for Hybrid Logic. HyLo@FLoC 2006: 15-27 - 2005
- [c44]Joachim Niehren, Jan Schwinghammer, Gert Smolka:
A Concurrent Lambda Calculus with Futures. FroCoS 2005: 248-263 - [c43]Guido Tack, Leif Kornstaedt, Gert Smolka:
Generic Pickling and Minimization. ML 2005: 79-103 - 2004
- [c42]Ralph Debusmann, Denys Duchier, Alexander Koller, Marco Kuhlmann, Gert Smolka, Stefan Thater:
A Relational Syntax-Semantics Interface Based on Dependency Grammar. COLING 2004 - [c41]Gert Smolka:
The Development of Oz and Mozart. MOZ 2004: 1 - [c40]Andreas Rossberg, Didier Le Botlan, Guido Tack, Thorsten Brunklaus, Gert Smolka:
Alice through the looking glass. Trends in Functional Programming 2004: 79-95 - 2000
- [j15]Gert Smolka:
Introduction. Constraints An Int. J. 5(1/2): 5 (2000) - [j14]Gert Smolka:
Guest Editor's Foreword. Nord. J. Comput. 7(4): 257 (2000) - [e3]Gert Smolka:
Programming Languages and Systems, 9th European Symposium on Programming, ESOP 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings. Lecture Notes in Computer Science 1782, Springer 2000, ISBN 3-540-67262-1 [contents]
1990 – 1999
- 1999
- [j13]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): 569-626 (1999) - 1998
- [c39]Gert Smolka:
Concurrent Constraint Programming Based on Functional Programming (Extended Abstract). ESOP 1998: 1-11 - 1997
- [j12]Andreas Podelski, Gert Smolka:
Situated Simplification. Theor. Comput. Sci. 173(1): 235-252 (1997) - [j11]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): 804-851 (1997) - [c38]Seif Haridi, Peter Van Roy, Gert Smolka:
An overview of the design of Distributed Oz. PASCO 1997: 176-187 - [c37]Gert Smolka:
Constraint Programming in Oz (Abstract). ILPS 1997: 37-38 - [e2]Gert Smolka:
Principles and Practice of Constraint Programming - CP97, Third International Conference, Linz, Austria, October 29 - November 1, 1997, Proceedings. Lecture Notes in Computer Science 1330, Springer 1997 [contents] - 1996
- [j10]Gert Smolka:
Constraints in OZ. ACM Comput. Surv. 28(4es): 75 (1996) - [j9]Martin Müller, Gert Smolka:
Oz: nebenläufige Programmierung mit Constraints. Künstliche Intell. 10(3): 55-61 (1996) - [c36]Gert Smolka:
The Oz Programming Language and System (Abstract). ASIAN 1996: 377 - [c35]Gert Smolka:
The Oz Programming Model. JELIA 1996: 251 - 1995
- [j8]Rolf Backofen, Gert Smolka:
A Complete and Recursive Feature Theory. Theor. Comput. Sci. 146(1&2): 243-268 (1995) - [c34]Andreas Podelski, Gert Smolka:
Situated Simplification. CP 1995: 328-344 - [c33]Gert Smolka:
The Oz Programming Model (Extended Abstract). Euro-Par 1995: 5-8 - [c32]Gert Smolka:
Oz: Concurrent Constraint Programming for Real. ICLP 1995: 13 - [c31]Andreas Podelski, Gert Smolka:
Operational Semantics of Constraint Logic Programs with Coroutining. ICLP 1995: 449-463 - [c30]Andreas Podelski, Gert Smolka:
Situated Simplification. ICLP 1995: 826 - [c29]Gert Smolka:
Objects in a higher-order concurrent constraint model with state. LMO 1995: 69-74 - [p3]Gert Smolka:
The Oz Programming Model. Computer Science Today 1995: 324-343 - 1994
- [j7]Gert Smolka, Ralf Treinen:
Records for Logic Programming. J. Log. Program. 18(3): 229-258 (1994) - [j6]Hassan Aït-Kaci, Andreas Podelski, Gert Smolka:
A Feature Constraint System for Logic Programming with Entailment. Theor. Comput. Sci. 122(1&2): 263-283 (1994) - [c28]Gert Smolka:
A Foundation for Higher-order Concurrent Constraint Programming. CCL 1994: 50-72 - [c27]Joachim Niehren, Gert Smolka:
A Confluent Relational Calculus for Higher-Order Programming with Constraints. CCL 1994: 89-104 - [c26]Andreas V. Hense, Gert Smolka:
A Record Calculus with Principal Types. CCL 1994: 219-236 - [c25]Christian Schulte, Gert Smolka, Jörg Würtz:
Encapsulated Search and Constraint Programming in Oz. PPCP 1994: 134-150 - [c24]Christian Schulte, Gert Smolka:
Encapsulated Search for Higher-order Concurrent Constraint Programming. ILPS 1994: 505-520 - [c23]Gert Smolka:
The Definition of Kernel Oz. Constraint Programming 1994: 251-292 - [i6]Rolf Backofen, Gert Smolka:
A Complete and Recursive Feature Theory. CoRR abs/cmp-lg/9406019 (1994) - 1993
- [j5]Franz Baader, Hans-Jürgen Bürckert, Bernhard Nebel
On the expressivity of feature logics with negation, functional uncertainty, and sort equations. J. Log. Lang. Inf. 2(1): 1-18 (1993) - [c22]Rolf Backofen, Gert Smolka:
A Complete and Recursive Feature Theory. ACL 1993: 193-200 - [c21]Gert Smolka:
A Survey of Oz - A Higher-order Concurrent Constraint Language. ICLP Workshop on Concurrent Constraint Programming 1993 - [c20]Martin Henz, Gert Smolka, Jörg Würtz:
Oz - A Programming Language for Multi-Agent Systems. IJCAI 1993: 404-409 - [c19]Gert Smolka, Martin Henz, Jörg Würtz:
Object-Oriented Concurrent Constraint Programming in Oz. KI 1993: 44-59 - [c18]Gert Smolka:
Nebenläfige Objekte und Logische Programmierung. WLP 1993: 7-9 - [e1]Christian Schulte, Gert Smolka:
Proceedings of the ICLP'93 Post-Conference Workshop on Concurrent Constraint Programming, Budapest, Hungary, June 24-25, 1993. 1993 [contents] - 1992
- [j4]Gert Smolka:
Feature-Constraint Logics for Unification Grammars. J. Log. Program. 12(1&2): 51-87 (1992) - [c17]Hassan Aït-Kaci, Andreas Podelski, Gert Smolka:
A Feature-Based Constraint System for Logic Programming with Entailment. FGCS 1992: 1012-1021 - [c16]Gert Smolka, Ralf Treinen:
Records for Logic Programming. JICSLP 1992: 240-254 - [c15]Andreas V. Hense, Gert Smolka:
A Verification of Extensible Record Types. IWAR 1992: 137-164 - [p2]Gert Smolka:
Residuation and Guarded Rules for Constraint Logic Programming. Informatik 1992: 387-400 - 1991
- [j3]Manfred Schmidt-Schauß, Gert Smolka:
Attributive Concept Descriptions with Complements. Artif. Intell. 48(1): 1-26 (1991) - [c14]Gert Smolka:
Residuation and Guarded Rules for Constraint Logic Programming. WCLP 1991: 405-419 - [c13]Bernhard Nebel, Gert Smolka:
Attribute Description Formalisms ... and the Rest of the World. Text Understanding in LILOG 1991: 439-452 - 1990
- [c12]Jürgen Müller, Franz Baader, Bernhard Nebel
Tutorial on Reasoning and Representation with Concept Languages. CADE 1990: 681
1980 – 1989
- 1989
- [b1]Gert Smolka:
Logic Programming over Polymorphically Order-Sorted Types. Kaiserslautern University of Technology, Germany, 1989, pp. 1-222 - [j2]Werner Nutt, Pierre Réty, Gert Smolka:
Basic Narrowing Revisited. J. Symb. Comput. 7(3/4): 295-317 (1989) - [j1]Gert Smolka, Hassan Aït-Kaci:
Inheritance Hierarchies: Semantics and Unification. J. Symb. Comput. 7(3/4): 343-370 (1989) - [c11]Daniel Hernández, Bernhard Nebel, Gert Smolka, Ipke Wachsmuth:
Fachseminar: Formale und kognitive Grundlagen von Wissensrepräsentationen. GWAI 1989: 476 - [c10]Gert Smolka:
Feature-Logik. GWAI 1989: 477-478 - [c9]Bernhard Nebel
Representation and Reasoning with Attributive Descriptions. Sorts and Types in Artificial Intelligence 1989: 112-139 - [i5]Manfred Schmidt-Schauß, Gert Smolka:
Attributive Concept Descriptions with Unions and Complements. IWBS Report 68 (1989) - [i4]Bernhard Nebel, Gert Smolka:
Representation and Reasoning with Attributive Descriptions. IWBS Report 81 (1989) - [i3]Gert Smolka:
Feature Constraint Logics for Unification Grammars. IWBS Report 93 (1989) - 1988
- [c8]Gert Smolka:
Type Logic. ADT 1988 - [c7]Gert Smolka:
Logic Programming with Polymorphically Order-Sorted Types. ALP 1988: 53-70 - [i2]Gert Smolka:
A Feature Logic with Subsorts. LILOG-Report 33 (1988) - [i1]Markus Höhfeld, Gert Smolka:
Definite Resolution over Constraint Languages. LILOG-Report 53 (1988) - 1986
- [c6]Gert Smolka:
Polymorphic Order-Sorted Algebra. ADT 1986 - [p1]Gert Smolka:
FRESH: A Higher-Order Language With Unification and Multiple Results. Logic Programming: Functions, Relations, and Equations 1986: 469-524 - 1984
- [c5]Gert Smolka:
Making Control and Data Flow in Logic Programs Explicit. LISP and Functional Programming 1984: 311-322 - 1982
- [c4]Gert Smolka:
Completeness of the Connection Graph Proof Procedure for Unit-Refutable Clause Sets. GWAI 1982: 191-204 - 1981
- [c3]Karl-Hans Bläsius, Norbert Eisinger, Jörg H. Siekmann, Gert Smolka, Alexander Herold, Christoph Walther:
The Markgraf Karl Refutation Procedure. IJCAI 1981: 511-518 - [c2]Jörg H. Siekmann, Gert Smolka:
Selection Heuristics, Deletion Strategies and N-Level Terminator Configurations for the Connection Graph Proof Procedure. GWAI 1981: 199-200 - 1980
- [c1]Norbert Eisinger, Jörg H. Siekmann, Gert Smolka, E. Unvericht, Christoph Walther:
Das Karlsruher Beweissystem. GI Jahrestagung 1980: 400-412
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 21:13 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: