Gert Smolka

According to our database1, Gert Smolka authored at least 109 papers between 1980 and 2019.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2019
Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory.
J. Autom. Reasoning, 2019

Call-by-Value Lambda Calculus as a Model of Computation in Coq.
J. Autom. Reasoning, 2019

On synthetic undecidability in coq, with an application to the entscheidungsproblem.
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018
Regular Language Representations in the Constructive Type Theory of Coq.
J. Autom. Reasoning, 2018

Verification of PCP-Related Computational Reductions in Coq.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Large model constructions for second-order ZF in dependent type theory.
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine.
Proceedings of the Programming Languages and Systems - 16th Asian Symposium, 2018

2017
Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga.
Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

Categoricity Results for Second-Order ZF in Dependent Type Theory.
Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq.
Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Equivalence of system f and ź2 in Coq based on context morphism lemmas.
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

Tower Induction and Up-to Techniques for CCS with Fixed Points.
Proceedings of the Relational and Algebraic Methods in Computer Science, 2017

2016
Completeness and Decidability Results for CTL in Constructive Type Theory.
J. Autom. Reasoning, 2016

Hereditarily Finite Sets in Constructive Type Theory.
Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

Two-Way Automata in Coq.
Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

Axiomatic semantics for compiler verification.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2015
Transfinite Constructions in Classical Type Theory.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

A Linear First-Order Functional Intermediate Language for Verified Compilers.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Completeness and Decidability of de Bruijn Substitution Algebra in Coq.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014
A Goal-Directed Decision Procedure for Hybrid PDL.
J. Autom. Reasoning, 2014

Completeness and Decidability Results for CTL in Coq.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013
Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification.
Proceedings of the 24th International Conference on Rewriting Techniques and Applications, 2013

A Constructive Theory of Regular Languages in Coq.
Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012
Constructive Completeness for Modal Logic with Transitive Closure.
Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011
Clausal Tableaux for Hybrid PDL.
Electr. Notes Theor. Comput. Sci., 2011

Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies
Logical Methods in Computer Science, 2011

Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2011

Incremental Decision Procedures for Modal Logic with Nominals and Eventualities.
Proceedings of the 24th International Workshop on Description Logics (DL 2011), 2011

Constructive Formalization of Hybrid Logic with Eventualities.
Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010
Spartacus: A Tableau Prover for Hybrid Logic.
Electr. Notes Theor. Comput. Sci., 2010

Analytic Tableaux for Simple Type Theory and its First-Order Fragment
Logical Methods in Computer Science, 2010

Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Terminating Tableaux for SOQ\mathcal{SOQ} with Number Restrictions on Transitive Roles.
Proceedings of the Theoretical Computer Science, 2010

Terminating Tableaux for Hybrid Logic with Eventualities.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009
Terminating Tableau Systems for Hybrid Logic with Difference and Converse.
Journal of Logic, Language and Information, 2009

Hybrid Tableaux for the Difference Modality.
Electr. Notes Theor. Comput. Sci., 2009

Extended First-Order Logic.
Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2009

Terminating Tableaux for the Basic Fragment of Simple Type Theory.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2009

Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles.
Proceedings of the 22nd International Workshop on Description Logics (DL 2009), 2009

2008
Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

Programmierung - eine Einführung in die Informatik mit Standard ML.
Oldenbourg, ISBN: 978-3-486-58601-5, 2008

2007
Higher-Order Syntax and Saturation Algorithms for Hybrid Logic.
Electr. Notes Theor. Comput. Sci., 2007

2006
Generic Pickling and Minimization.
Electr. Notes Theor. Comput. Sci., 2006

Multi-Dimensional Dependency Grammar as Multigraph Description.
Proceedings of the Nineteenth International Florida Artificial Intelligence Research Society Conference, 2006

Generating Propagators for Finite Set Constraints.
Proceedings of the Principles and Practice of Constraint Programming, 2006

2005
A Concurrent Lambda Calculus with Futures.
Proceedings of the Frontiers of Combining Systems, 5th International Workshop, 2005

2004
Alice through the looking glass.
Proceedings of the Revised Selected Papers from the Fifth Symposium on Trends in Functional Programming, 2004

The Development of Oz and Mozart.
Proceedings of the Multiparadigm Programming in Mozart/Oz, Second International Conference, 2004

A Relational Syntax-Semantics Interface Based on Dependency Grammar.
Proceedings of the COLING 2004, 2004

2000
Guest Editor's Foreword.
Nord. J. Comput., 2000

Introduction.
Constraints, 2000

1999
Efficient logic variables for distributed computing.
ACM Trans. Program. Lang. Syst., 1999

1998
Concurrent Constraint Programming Based on Functional Programming (Extended Abstract).
Proceedings of the Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28, 1998

1997
Mobile Objects in Distributed Oz.
ACM Trans. Program. Lang. Syst., 1997

Constraint Programming in Oz (Abstract).
Proceedings of the Logic Programming, 1997

An overview of the design of Distributed Oz.
Proceedings of the 2nd International Workshop on Parallel Symbolic Computation, 1997

1996
Oz: nebenläufige Programmierung mit Constraints.
KI, 1996

Constraints in OZ.
ACM Comput. Surv., 1996

The Oz Programming Model.
Proceedings of the Logics in Artificial Intelligence, European Workshop, 1996

The Oz Programming Language and System (Abstract).
Proceedings of the Concurrency and Parallelism, 1996

1995
Objects in a higher-order concurrent constraint model with state.
Proceedings of the Actes des journées Langages et Modèles à Objets, 1995

Oz: Concurrent Constraint Programming for Real.
Proceedings of the Logic Programming, 1995

Situated Simplification.
Proceedings of the Logic Programming, 1995

Operational Semantics of Constraint Logic Programs with Coroutining.
Proceedings of the Logic Programming, 1995

The Oz Programming Model (Extended Abstract).
Proceedings of the Euro-Par '95 Parallel Processing, 1995

Situated Simplification.
Proceedings of the Principles and Practice of Constraint Programming, 1995

1994
A Feature Constraint System for Logic Programming with Entailment.
Theor. Comput. Sci., 1994

The Definition of Kernel Oz
Proceedings of the Constraint Programming: Basics and Trends, Châtillon Spring School, 1994

Encapsulated Search for Higher-order Concurrent Constraint Programming.
Proceedings of the Logic Programming, 1994

Encapsulated Search and Constraint Programming in Oz.
Proceedings of the Principles and Practice of Constraint Programming, 1994

A Foundation for Higher-order Concurrent Constraint Programming.
Proceedings of the Constraints in Computational Logics, First International Conference, 1994

A Confluent Relational Calculus for Higher-Order Programming with Constraints.
Proceedings of the Constraints in Computational Logics, First International Conference, 1994

A Record Calculus with Principal Types.
Proceedings of the Constraints in Computational Logics, First International Conference, 1994

1993
On the expressivity of feature logics with negation, functional uncertainty, and sort equations.
Journal of Logic, Language and Information, 1993

Nebenläfige Objekte und Logische Programmierung.
Proceedings of the 9. Workshop Logische Programmierung, 1993

Object-Oriented Concurrent Constraint Programming in Oz.
Proceedings of the Grundlagen und Anwendungen der Künstlichen Intelligenz, 1993

Oz - A Programming Language for Multi-Agent Systems.
Proceedings of the 13th International Joint Conference on Artificial Intelligence. Chambéry, France, August 28, 1993

A Survey of Oz - A Higher-order Concurrent Constraint Language.
Proceedings of the ICLP'93 Post-Conference Workshop on Concurrent Constraint Programming, 1993

A Complete and Recursive Feature Theory.
Proceedings of the 31st Annual Meeting of the Association for Computational Linguistics, 1993

1992
Feature-Constraint Logics for Unification Grammars.
J. Log. Program., 1992

A Verification of Extensible Record Types.
Proceedings of the Automated Reasoning, 1992

Records for Logic Programming.
Proceedings of the Logic Programming, 1992

A Feature-Based Constraint System for Logic Programming with Entailment.
Proceedings of the International Conference on Fifth Generation Computer Systems. FGCS 1992, 1992

1991
Attribute Description Formalisms ... and the Rest of the World.
Proceedings of the Text Understanding in LILOG, 1991

Attributive Concept Descriptions with Complements.
Artif. Intell., 1991

Residuation and Guarded Rules for Constraint Logic Programming.
Proceedings of the Constraint Logic Programming, 1991

1990
Tutorial on Reasoning and Representation with Concept Languages.
Proceedings of the 10th International Conference on Automated Deduction, 1990

1989
Feature Constraint Logics for Unification Grammars
IWBS Report, 1989

Representation and Reasoning with Attributive Descriptions
IWBS Report, 1989

Attributive Concept Descriptions with Unions and Complements
IWBS Report, 1989

Logic Programming over Polymorphically Order-Sorted Types.
PhD thesis, 1989

Inheritance Hierarchies: Semantics and Unification.
J. Symb. Comput., 1989

Basic Narrowing Revisited.
J. Symb. Comput., 1989

Representation and Reasoning with Attributive Descriptions.
Proceedings of the Sorts and Types in Artificial Intelligence, 1989

Feature-Logik.
Proceedings of the GWAI-89, 1989

Fachseminar: Formale und kognitive Grundlagen von Wissensrepräsentationen.
Proceedings of the GWAI-89, 1989

1988
Definite Resolution over Constraint Languages
LILOG-Report, 1988

A Feature Logic with Subsorts
LILOG-Report, 1988

Logic Programming with Polymorphically Order-Sorted Types.
Proceedings of the Algebraic and Logic Programming, 1988

Type Logic.
Proceedings of the 6st Workshop on Abstract Data Type, 1988. University of Berlin, Germany, 1988

1986
Polymorphic Order-Sorted Algebra.
Proceedings of the 4st Workshop on Abstract Data Type, 1986

FRESH: A Higher-Order Language With Unification and Multiple Results.
Proceedings of the Logic Programming: Functions, Relations, and Equations, 1986

1984
Making Control and Data Flow in Logic Programs Explicit.
Proceedings of the 1984 ACM Conference on LISP and Functional Programming, 1984

1982
Completeness of the Connection Graph Proof Procedure for Unit-Refutable Clause Sets.
Proceedings of the GWAI-82, 6th German Workshop on Artificial Intelligence, Bad Honnef, Germany, September 27, 1982

1981
Selection Heuristics, Deletion Strategies and N-Level Terminator Configurations for the Connection Graph Proof Procedure.
Proceedings of the GWAI-81, 1981

The Markgraf Karl Refutation Procedure.
Proceedings of the 7th International Joint Conference on Artificial Intelligence, 1981

1980
Das Karlsruher Beweissystem.
Proceedings of the GI - 10. Jahrestagung, Saarbrücken, 30. September, 1980


  Loading...