Gert Smolka - RankMe

129 papers A* 3A 8B 29C 1Misc 2Journal 38Unranked 42

Year	Rank	Type	Title / Venue / Authors
2023	B	`conf`	A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). CPP Yannick Forster, Felix Jahn, Gert Smolka
2021	B	`conf`	A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. ITP Yannick Forster, Fabian Kunze, Gert Smolka, Maxi Wuttke
2020	J	`jnl`	A history of the Oz multiparadigm language. Proc. ACM Program. Lang. Peter Van Roy, Seif Haridi, Christian Schulte, Gert Smolka
2019	J	`jnl`	Call-by-Value Lambda Calculus as a Model of Computation in Coq. J. Autom. Reason. Yannick Forster, Gert Smolka
2019	J	`jnl`	Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory. J. Autom. Reason. Dominik Kirst, Gert Smolka
2019	B	`conf`	On synthetic undecidability in coq, with an application to the entscheidungsproblem. CPP Yannick Forster, Dominik Kirst, Gert Smolka
2018	J	`jnl`	Constructive Analysis of S1S and Büchi Automata. CoRR Moritz Lichter, Gert Smolka
2018	B	`conf`	Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine. APLAS Fabian Kunze, Gert Smolka, Yannick Forster
2018	J	`jnl`	Formal Small-step Verification of a Call-by-value Lambda Calculus Machine. CoRR Fabian Kunze, Gert Smolka, Yannick Forster
2018	B	`conf`	Large model constructions for second-order ZF in dependent type theory. CPP Dominik Kirst, Gert Smolka
2018	J	`jnl`	Regular Language Representations in the Constructive Type Theory of Coq. J. Autom. Reason. Christian Doczkal, Gert Smolka
2018	B	`conf`	Verification of PCP-Related Computational Reductions in Coq. ITP Yannick Forster, Edith Heiter, Gert Smolka
2017	B	`conf`	Categoricity Results for Second-Order ZF in Dependent Type Theory. ITP Dominik Kirst, Gert Smolka
2017	B	`conf`	Equivalence of system f and ź2 in Coq based on context morphism lemmas. CPP Jonas Kaiser, Tobias Tebbi, Gert Smolka
2017	B	`conf`	Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. FSCD Jonas Kaiser, Brigitte Pientka, Gert Smolka
2017	C	`conf`	Tower Induction and Up-to Techniques for CCS with Fixed Points. RAMiCS Steven Schäfer, Gert Smolka
2017	J	`jnl`	Verification of PCP-Related Computational Reductions in Coq. CoRR Yannick Forster, Edith Heiter, Gert Smolka
2017	B	`conf`	Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. ITP Yannick Forster, Gert Smolka
2016	J	`jnl`	An Inductive Proof Method for Simulation-based Compiler Correctness. CoRR Sigurd Schneider, Gert Smolka, Sebastian Hack
2016	B	`conf`	Axiomatic semantics for compiler verification. CPP Steven Schäfer, Sigurd Schneider, Gert Smolka
2016	J	`jnl`	Completeness and Decidability Results for CTL in Constructive Type Theory. J. Autom. Reason. Christian Doczkal, Gert Smolka
2016	B	`conf`	Hereditarily Finite Sets in Constructive Type Theory. ITP Gert Smolka, Kathrin Stark
2016	B	`conf`	Two-Way Automata in Coq. ITP Christian Doczkal, Gert Smolka
2015	J	`jnl`	A First-Order Functional Intermediate Language for Verified Compilers. CoRR Sigurd Schneider, Gert Smolka, Sebastian Hack
2015	B	`conf`	A Linear First-Order Functional Intermediate Language for Verified Compilers. ITP Sigurd Schneider, Gert Smolka, Sebastian Hack
2015	B	`conf`	Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. ITP Steven Schäfer, Tobias Tebbi, Gert Smolka
2015	B	`conf`	Completeness and Decidability of de Bruijn Substitution Algebra in Coq. CPP Steven Schäfer, Gert Smolka, Tobias Tebbi
2015	B	`conf`	Transfinite Constructions in Classical Type Theory. ITP Gert Smolka, Steven Schäfer, Christian Doczkal
2014	J	`jnl`	A Goal-Directed Decision Procedure for Hybrid PDL. J. Autom. Reason. Mark Kaminski, Gert Smolka
2014	B	`conf`	Completeness and Decidability Results for CTL in Coq. ITP Christian Doczkal, Gert Smolka
2013	B	`conf`	A Constructive Theory of Regular Languages in Coq. CPP Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka
2013	—	`conf`	Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification. RTA Gert Smolka, Tobias Tebbi
2012	B	`conf`	Constructive Completeness for Modal Logic with Transitive Closure. CPP Christian Doczkal, Gert Smolka
2012	J	`jnl`	Correctness of an Incremental and Worst-Case Optimal Decision Procedure for Modal Logic with Eventualities CoRR Mark Kaminski, Gert Smolka
2011	—	`conf`	Clausal Tableaux for Hybrid PDL. M4M/LAMAS Mark Kaminski, Gert Smolka
2011	B	`conf`	Constructive Formalization of Hybrid Logic with Eventualities. CPP Christian Doczkal, Gert Smolka
2011	B	`conf`	Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics. TABLEAUX Mark Kaminski, Thomas Schneider, Gert Smolka
2011	—	`conf`	Incremental Decision Procedures for Modal Logic with Nominals and Eventualities. Description Logics Gert Smolka
2011	J	`jnl`	Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies Log. Methods Comput. Sci. Mark Kaminski, Sigurd Schneider, Gert Smolka
2010	J	`jnl`	A Minimal Propositional Type Theory CoRR Mark Kaminski, Gert Smolka
2010	J	`jnl`	Analytic Tableaux for Simple Type Theory and its First-Order Fragment Log. Methods Comput. Sci. Chad E. Brown, Gert Smolka
2010	—	`conf`	Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference. LPAR (Yogyakarta) Mark Kaminski, Gert Smolka
2010	—	`conf`	Terminating Tableaux for IFIP TCS Mark Kaminski, Gert Smolka
2010	A	`conf`	Terminating Tableaux for Hybrid Logic with Eventualities. IJCAR Mark Kaminski, Gert Smolka
2009	—	`conf`	Extended First-Order Logic. TPHOLs Chad E. Brown, Gert Smolka
2009	—	`conf`	Spartacus: A Tableau Prover for Hybrid Logic. M4M Daniel Götzmann, Mark Kaminski, Gert Smolka
2009	J	`jnl`	Terminating Tableau Systems for Hybrid Logic with Difference and Converse. J. Log. Lang. Inf. Mark Kaminski, Gert Smolka
2009	B	`conf`	Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies. TABLEAUX Mark Kaminski, Sigurd Schneider, Gert Smolka
2009	—	`conf`	Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles. Description Logics Mark Kaminski, Gert Smolka
2009	B	`conf`	Terminating Tableaux for the Basic Fragment of Simple Type Theory. TABLEAUX Chad E. Brown, Gert Smolka
2008	—	`book`	Programmierung - eine Einführung in die Informatik mit Standard ML. Gert Smolka
2008	A	`conf`	Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse. IJCAR Mark Kaminski, Gert Smolka
2007	—	`conf`	Hybrid Tableaux for the Difference Modality. M4M Mark Kaminski, Gert Smolka
2006	J	`jnl`	A concurrent lambda calculus with futures. Theor. Comput. Sci. Joachim Niehren, Jan Schwinghammer, Gert Smolka
2006	A	`conf`	Generating Propagators for Finite Set Constraints. CP Guido Tack, Christian Schulte, Gert Smolka
2006	—	`conf`	Higher-Order Syntax and Saturation Algorithms for Hybrid Logic. HyLo@FLoC Moritz Hardt, Gert Smolka
2006	Misc	`conf`	Multi-Dimensional Dependency Grammar as Multigraph Description. FLAIRS Ralph Debusmann, Gert Smolka
2005	—	`conf`	A Concurrent Lambda Calculus with Futures. FroCoS Joachim Niehren, Jan Schwinghammer, Gert Smolka
2005	—	`conf`	Generic Pickling and Minimization. ML Guido Tack, Leif Kornstaedt, Gert Smolka
2004	B	`conf`	A Relational Syntax-Semantics Interface Based on Dependency Grammar. COLING Ralph Debusmann, Denys Duchier, Alexander Koller, Marco Kuhlmann, Gert Smolka, Stefan Thater
2004	—	`conf`	Alice through the looking glass. Trends in Functional Programming Andreas Rossberg, Didier Le Botlan, Guido Tack, Thorsten Brunklaus, Gert Smolka
2004	—	`conf`	The Development of Oz and Mozart. MOZ Gert Smolka
2000	J	`jnl`	Guest Editor's Foreword. Nord. J. Comput. Gert Smolka
2000	J	`jnl`	Introduction. Constraints An Int. J. Gert Smolka
2000	A	`ed.`	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 ESOP Gert Smolka
1999	J	`jnl`	Efficient logic variables for distributed computing. ACM Trans. Program. Lang. Syst. Seif Haridi, Peter Van Roy, Per Brand, Michael Mehl, Ralf Scheidhauer, Gert Smolka
1998	A	`conf`	Concurrent Constraint Programming Based on Functional Programming (Extended Abstract). ESOP Gert Smolka
1997	—	`conf`	An overview of the design of Distributed Oz. PASCO Seif Haridi, Peter Van Roy, Gert Smolka
1997	—	`conf`	Constraint Programming in Oz (Abstract). ILPS Gert Smolka
1997	J	`jnl`	Mobile Objects in Distributed Oz. ACM Trans. Program. Lang. Syst. Peter Van Roy, Seif Haridi, Per Brand, Gert Smolka, Michael Mehl, Ralf Scheidhauer
1997	A	`ed.`	Principles and Practice of Constraint Programming - CP97, Third International Conference, Linz, Austria, October 29 - November 1, 1997, Proceedings CP Gert Smolka
1997	J	`jnl`	Situated Simplification. Theor. Comput. Sci. Andreas Podelski, Gert Smolka
1996	J	`jnl`	Constraints in OZ. ACM Comput. Surv. Gert Smolka
1996	J	`jnl`	Oz: nebenläufige Programmierung mit Constraints. Künstliche Intell. Martin Müller, Gert Smolka
1996	—	`conf`	The Oz Programming Language and System (Abstract). ASIAN Gert Smolka
1996	B	`conf`	The Oz Programming Model. JELIA Gert Smolka
1995	J	`jnl`	A Complete and Recursive Feature Theory. Theor. Comput. Sci. Rolf Backofen, Gert Smolka
1995	—	`conf`	Objects in a higher-order concurrent constraint model with state. LMO Gert Smolka
1995	B	`conf`	Operational Semantics of Constraint Logic Programs with Coroutining. ICLP Andreas Podelski, Gert Smolka
1995	B	`conf`	Oz: Concurrent Constraint Programming for Real. ICLP Gert Smolka
1995	A	`conf`	Situated Simplification. CP Andreas Podelski, Gert Smolka
1995	B	`conf`	Situated Simplification. ICLP Andreas Podelski, Gert Smolka
1995	—	`conf`	The Oz Programming Model (Extended Abstract). Euro-Par Gert Smolka
1995	—	`ch.`	The Oz Programming Model. Computer Science Today Gert Smolka
1994	J	`jnl`	A Complete and Recursive Feature Theory. CoRR Rolf Backofen, Gert Smolka
1994	—	`conf`	A Confluent Relational Calculus for Higher-Order Programming with Constraints. CCL Joachim Niehren, Gert Smolka
1994	J	`jnl`	A Feature Constraint System for Logic Programming with Entailment. Theor. Comput. Sci. Hassan Aït-Kaci, Andreas Podelski, Gert Smolka
1994	—	`conf`	A Foundation for Higher-order Concurrent Constraint Programming. CCL Gert Smolka
1994	—	`conf`	A Record Calculus with Principal Types. CCL Andreas V. Hense, Gert Smolka
1994	—	`conf`	Encapsulated Search and Constraint Programming in Oz. PPCP Christian Schulte, Gert Smolka, Jörg Würtz
1994	—	`conf`	Encapsulated Search for Higher-order Concurrent Constraint Programming. ILPS Christian Schulte, Gert Smolka
1994	J	`jnl`	Records for Logic Programming. J. Log. Program. Gert Smolka, Ralf Treinen
1994	—	`conf`	The Definition of Kernel Oz Constraint Programming Gert Smolka
1993	A*	`conf`	A Complete and Recursive Feature Theory. ACL Rolf Backofen, Gert Smolka
1993	—	`conf`	A Survey of Oz - A Higher-order Concurrent Constraint Language. ICLP Workshop on Concurrent Constraint Programming Gert Smolka
1993	—	`conf`	Nebenläfige Objekte und Logische Programmierung. WLP Gert Smolka
1993	Misc	`conf`	Object-Oriented Concurrent Constraint Programming in Oz. KI Gert Smolka, Martin Henz, Jörg Würtz
1993	J	`jnl`	On the expressivity of feature logics with negation, functional uncertainty, and sort equations. J. Log. Lang. Inf. Franz Baader, Hans-Jürgen Bürckert, Bernhard Nebel, Werner Nutt, Gert Smolka
1993	A*	`conf`	Oz - A Programming Language for Multi-Agent Systems. IJCAI Martin Henz, Gert Smolka, Jörg Würtz
1993	—	`ed.`	Proceedings of the ICLP'93 Post-Conference Workshop on Concurrent Constraint Programming, Budapest, Hungary, June 24-25, 1993 ICLP Workshop on Concurrent Constraint Programming Christian Schulte, Gert Smolka
1992	—	`conf`	A Feature-Based Constraint System for Logic Programming with Entailment. FGCS Hassan Aït-Kaci, Andreas Podelski, Gert Smolka
1992	—	`conf`	A Verification of Extensible Record Types. IWAR Andreas V. Hense, Gert Smolka
1992	J	`jnl`	Feature-Constraint Logics for Unification Grammars. J. Log. Program. Gert Smolka
1992	—	`conf`	Records for Logic Programming. JICSLP Gert Smolka, Ralf Treinen
1992	—	`ch.`	Residuation and Guarded Rules for Constraint Logic Programming. Informatik Gert Smolka
1991	—	`conf`	Attribute Description Formalisms ... and the Rest of the World. Text Understanding in LILOG Bernhard Nebel, Gert Smolka
1991	J	`jnl`	Attributive Concept Descriptions with Complements. Artif. Intell. Manfred Schmidt-Schauß, Gert Smolka
1991	—	`conf`	Residuation and Guarded Rules for Constraint Logic Programming. WCLP Gert Smolka
1990	A	`conf`	Tutorial on Reasoning and Representation with Concept Languages. CADE Jürgen Müller, Franz Baader, Bernhard Nebel, Werner Nutt, Gert Smolka
1989	J	`jnl`	Attributive Concept Descriptions with Unions and Complements IWBS Report Manfred Schmidt-Schauß, Gert Smolka
1989	J	`jnl`	Basic Narrowing Revisited. J. Symb. Comput. Werner Nutt, Pierre Réty, Gert Smolka
1989	—	`conf`	Fachseminar: Formale und kognitive Grundlagen von Wissensrepräsentationen. GWAI Daniel Hernández, Bernhard Nebel, Gert Smolka, Ipke Wachsmuth
1989	J	`jnl`	Feature Constraint Logics for Unification Grammars IWBS Report Gert Smolka
1989	—	`conf`	Feature-Logik. GWAI Gert Smolka
1989	J	`jnl`	Inheritance Hierarchies: Semantics and Unification. J. Symb. Comput. Gert Smolka, Hassan Aït-Kaci
1989	—	`—`	Logic Programming over Polymorphically Order-Sorted Types. Gert Smolka
1989	J	`jnl`	Representation and Reasoning with Attributive Descriptions IWBS Report Bernhard Nebel, Gert Smolka
1989	—	`conf`	Representation and Reasoning with Attributive Descriptions. Sorts and Types in Artificial Intelligence Bernhard Nebel, Gert Smolka
1988	J	`jnl`	A Feature Logic with Subsorts LILOG-Report Gert Smolka
1988	J	`jnl`	Definite Resolution over Constraint Languages LILOG-Report Markus Höhfeld, Gert Smolka
1988	—	`conf`	Logic Programming with Polymorphically Order-Sorted Types. ALP Gert Smolka
1988	—	`conf`	Type Logic. ADT Gert Smolka
1986	—	`ch.`	FRESH: A Higher-Order Language With Unification and Multiple Results. Logic Programming: Functions, Relations, and Equations Gert Smolka
1986	—	`conf`	Polymorphic Order-Sorted Algebra. ADT Gert Smolka
1984	—	`conf`	Making Control and Data Flow in Logic Programs Explicit. LISP and Functional Programming Gert Smolka
1982	—	`conf`	Completeness of the Connection Graph Proof Procedure for Unit-Refutable Clause Sets. GWAI Gert Smolka
1981	—	`conf`	Selection Heuristics, Deletion Strategies and N-Level Terminator Configurations for the Connection Graph Proof Procedure. GWAI Jörg H. Siekmann, Gert Smolka
1981	A*	`conf`	The Markgraf Karl Refutation Procedure. IJCAI Karl-Hans Bläsius, Norbert Eisinger, Jörg H. Siekmann, Gert Smolka, Alexander Herold, Christoph Walther
1980	—	`conf`	Das Karlsruher Beweissystem. GI Jahrestagung Norbert Eisinger, Jörg H. Siekmann, Gert Smolka, E. Unvericht, Christoph Walther