Tobias Nipkow

J. Autom. Reason., June, 2024

Alpha-Beta Pruning.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

Region Quadtrees.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

A Verified Earley Parser.

[BibT_eX]

[DOI]

Martin Rau

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

Alpha-Beta Pruning Verified (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

Region Quadtrees Verified.

[BibT_eX]

[DOI]

Proceedings of the Taming the Infinities of Concurrency, 2024

2023

A Formalization and Proof Checker for Isabelle's Metalogic.

[BibT_eX]

[DOI]

Simon Roßkopf

J. Autom. Reason., 2023

Real-Time Double-Ended Queue Verified (Proof Pearl).

[BibT_eX]

[DOI]

Balázs Tóth

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

Verification of NP-Hardness Reduction Functions for Exact Lattice Problems.

[BibT_eX]

[DOI]

Katharina Kreuzer

Proceedings of the Automated Deduction - CADE 29, 2023

2022

Verified Approximation Algorithms.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2022

A Verified Implementation of B+-Trees in Isabelle/HOL.

[BibT_eX]

[DOI]

Niels Mündler

CoRR, 2022

Real-Time Double-Ended Queue.

[BibT_eX]

[DOI]

Balázs Tóth

Arch. Formal Proofs, 2022

A Verified Implementation of B+-Trees in Isabelle/HOL.

[BibT_eX]

[DOI]

Niels Mündler

Proceedings of the Theoretical Aspects of Computing - ICTAC 2022, 2022

2021

Isabelle's Metalogic: Formalization and Proof Checker.

[BibT_eX]

[DOI]

Simon Roßkopf

Arch. Formal Proofs, 2021

Gale-Shapley Algorithm.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

Teaching algorithms and data structures with a proof assistant (invited talk).

[BibT_eX]

[DOI]

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

A Verified Decision Procedure for Orders in Isabelle/HOL.

[BibT_eX]

[DOI]

Lukas Stevens

Proceedings of the Automated Technology for Verification and Analysis, 2021

2020

Verified Analysis of Random Binary Tree Structures.

[BibT_eX]

[DOI]

Max W. Haslbeck

J. Autom. Reason., 2020

Closest Pair of Points Algorithms.

[BibT_eX]

[DOI]

Martin Rau

Arch. Formal Proofs, 2020

Verified Approximation Algorithms.

[BibT_eX]

[DOI]

Robin Eßmann

Simon Robillard

Arch. Formal Proofs, 2020

Proof pearl: Braun trees.

[BibT_eX]

[DOI]

Thomas Sewell

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

Verification of Closest Pair of Points Algorithms.

[BibT_eX]

[DOI]

Martin Rau

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Verified Textbook Algorithms - A Biased Survey.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2020

2019

Amortized Complexity Verified.

[BibT_eX]

[DOI]

Hauke Brinkop

J. Autom. Reason., 2019

From LCF to Isabelle/HOL.

[BibT_eX]

[DOI]

Makarius Wenzel

Formal Aspects Comput., 2019

Trustworthy Graph Algorithms.

[BibT_eX]

[DOI]

Mohammad Abdulaziz

Kurt Mehlhorn

CoRR, 2019

Priority Search Trees.

[BibT_eX]

[DOI]

Peter Lammich

Arch. Formal Proofs, 2019

Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra.

[BibT_eX]

[DOI]

Peter Lammich

Arch. Formal Proofs, 2019

Trustworthy Graph Algorithms (Invited Talk).

[BibT_eX]

[DOI]

Mohammad Abdulaziz

Kurt Mehlhorn

Proceedings of the 44th International Symposium on Mathematical Foundations of Computer Science, 2019

Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra.

[BibT_eX]

[DOI]

Peter Lammich

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

2018

A Verified Compiler from Isabelle/HOL to CakeML.

[BibT_eX]

[DOI]

Lars Hupel

Dataset, April, 2018

Monadification, Memoization and Dynamic Programming.

[BibT_eX]

[DOI]

Simon Wimmer

Shuwei Hu

Arch. Formal Proofs, 2018

Optimal Binary Search Trees.

[BibT_eX]

[DOI]

Dániel Somogyi

Arch. Formal Proofs, 2018

Weight-Balanced Trees.

[BibT_eX]

[DOI]

Stefan Dirix

Arch. Formal Proofs, 2018

Hoare Logics for Time Bounds.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

Treaps.

[BibT_eX]

[DOI]

Max W. Haslbeck

Arch. Formal Proofs, 2018

Hoare Logics for Time Bounds - A Study in Meta Theory.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Verified Memoization and Dynamic Programming.

[BibT_eX]

[DOI]

Simon Wimmer

Shuwei Hu

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

A Verified Compiler from Isabelle/HOL to CakeML.

[BibT_eX]

[DOI]

Lars Hupel

Proceedings of the Programming Languages and Systems, 2018

2017

Root-Balanced Tree.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Propositional Proof Systems.

[BibT_eX]

[DOI]

Julius Michaelis

Arch. Formal Proofs, 2017

Formalized Proof Systems for Propositional Logic.

[BibT_eX]

[DOI]

Julius Michaelis

Proceedings of the 23rd International Conference on Types for Proofs and Programs, 2017

Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 13th International Conference, 2017

Verified Root-Balanced Trees.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

Software-Verifikation.

[BibT_eX]

[DOI]

Proceedings of the 50 Jahre Universitäts-Informatik in München, 2017

2016

Abstract Interpretation of Annotated Commands.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

Analysis of List Update Algorithms.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

Pairing Heap.

[BibT_eX]

[DOI]

Hauke Brinkop

Arch. Formal Proofs, 2016

Verified Analysis of Functional Data Structures.

[BibT_eX]

[DOI]

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

Automatic Functional Correctness Proofs for Functional Search Trees.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

Verified Analysis of List Update Algorithms.

[BibT_eX]

[DOI]

Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2016

2015

Verified decision procedures for MSO on words based on derivatives of regular expressions.

[BibT_eX]

[DOI]

J. Funct. Program., 2015

A formal proof of the Kepler conjecture.

[BibT_eX]

[DOI]

CoRR, 2015

Parameterized Dynamic Tables.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2015

Trie.

[BibT_eX]

[DOI]

Andreas Lochbihler

Arch. Formal Proofs, 2015

Mining the Archive of Formal Proofs.

[BibT_eX]

[DOI]

Max W. Haslbeck

Daniel Matichuk

Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

2014

Applications of Interactive Proof to Data Flow Analysis and Security.

[BibT_eX]

[DOI]

Proceedings of the Software Systems Safety, 2014

Making security type systems less ad hoc.

[BibT_eX]

[DOI]

it Inf. Technol., 2014

Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Unified Decision Procedures for Regular Expression Equivalence.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Priority Queues Based on Braun Trees.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Skew Heap.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Splay Tree.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Amortized Complexity Verified.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Boolean Expression Checkers.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

A Fully Verified Executable LTL Model Checker.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

A Verified Compiler for Probability Density Functions.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Experience report: the next 1100 Haskell programmers.

[BibT_eX]

[DOI]

Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, 2014

Concrete Semantics - With Isabelle/HOL

[BibT_eX]

[DOI]

Springer, ISBN: 978-3-319-10542-0, 2014

2013

Formal Verification of Language-Based Concurrent Noninterference.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2013

Deduction and Arithmetic (Dagstuhl Seminar 13411).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2013

A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2013

Data Refinement in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Formalizing Probabilistic Noninterference.

[BibT_eX]

[DOI]

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference.

[BibT_eX]

[DOI]

Proceedings of the Algebra and Coalgebra in Computer Science, 2013

2012

Interactive Proof: Introduction to Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the Software Safety and Security - Tools for Analysis and Verification, 2012

A compiled implementation of normalisation by evaluation.

[BibT_eX]

[DOI]

Klaus Aehlig

Florian Haftmann

J. Funct. Program., 2012

Proof Pearl: Regular Expression Equivalence and Relation Algebra.

[BibT_eX]

[DOI]

Alexander Krauss

J. Autom. Reason., 2012

Interactive verification of Markov chains: Two distributed protocol case studies

[BibT_eX]

[DOI]

Proceedings of the Proceedings Quantities in Formal Methods, 2012

Markov Models.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2012

Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Verifying pCTL Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Proving Concurrent Noninterference.

[BibT_eX]

[DOI]

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011

Majority Vote Algorithm Revisited Again.

[BibT_eX]

[DOI]

Int. J. Softw. Informatics, 2011

Gauss-Jordan Elimination for Matrices Represented as Functions.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2011

Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Automatic Proof and Disproof in Isabelle/HOL.

[BibT_eX]

[DOI]

Lukas Bulwahn

Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

Proof Pearl: The Marriage Theorem.

[BibT_eX]

[DOI]

Dongchen Jiang

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

Extending Hindley-Milner Type Inference with Coercive Structural Subtyping.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011

2010

Linear Quantifier Elimination.

[BibT_eX]

[DOI]

J. Autom. Reason., 2010

Deduktion: von der Theorie zur Anwendung.

[BibT_eX]

[DOI]

Franz Baader

Bernhard Beckert

Inform. Spektrum, 2010

A Revision of the Proof of the Kepler Conjecture.

[BibT_eX]

[DOI]

Discret. Comput. Geom., 2010

List Index.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2010

Regular Sets and Expressions.

[BibT_eX]

[DOI]

Alexander Krauss

Arch. Formal Proofs, 2010

Hall's Marriage Theorem.

[BibT_eX]

[DOI]

Dongchen Jiang

Arch. Formal Proofs, 2010

Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Code Generation via Higher-Order Rewrite Systems.

[BibT_eX]

[DOI]

Florian Haftmann

Proceedings of the Functional and Logic Programming, 10th International Symposium, 2010

Sledgehammer: Judgement Day.

[BibT_eX]

[DOI]

Sascha Böhme

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

Social Choice Theory in HOL.

[BibT_eX]

[DOI]

J. Autom. Reason., 2009

Flyspeck II: the basic linear programs.

[BibT_eX]

[DOI]

Steven Obua

Ann. Math. Artif. Intell., 2009

09411 Executive Summary - Interaction versus Automation: The two Faces of Deductions.

[BibT_eX]

[DOI]

Proceedings of the Interaction versus Automation: The two Faces of Deduction, 04.10., 2009

09411 Abstracts Collection - Interaction versus Automation: The two Faces of Deduction.

[BibT_eX]

[DOI]

Proceedings of the Interaction versus Automation: The two Faces of Deduction, 04.10., 2009

2008

Proof Synthesis and Reflection for Linear Arithmetic.

[BibT_eX]

[DOI]

Amine Chaieb

J. Autom. Reason., 2008

Preface.

[BibT_eX]

[DOI]

J. Autom. Reason., 2008

Fun With Tilings.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2008

Arrow and Gibbard-Satterthwaite.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2008

Fun With Functions.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2008

Quantifier Elimination for Linear Arithmetic.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2008

Normalization by Evaluation.

[BibT_eX]

[DOI]

Klaus Aehlig

Arch. Formal Proofs, 2008

The Isabelle Framework.

[BibT_eX]

[DOI]

Makarius Wenzel

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

A Compiled Implementation of Normalization by Evaluation.

[BibT_eX]

[DOI]

Klaus Aehlig

Florian Haftmann

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

2007

Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL.

[BibT_eX]

[DOI]

Lukas Bulwahn

Alexander Krauss

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

C++ ist typsicher? Garantiert!

[BibT_eX]

[DOI]

Proceedings of the Software Engineering 2007, 2007

Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic.

[BibT_eX]

[DOI]

Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

2006

A machine-checked model for a Java-like language, virtual machine, and compiler.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2006

Preface.

[BibT_eX]

[DOI]

Stephan Merz

Proceedings of the 6th International Workshop on Automated Verification of Critical Systems, 2006

Hotel Key Card System.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2006

Abstract Hoare Logics.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2006

Flyspeck I: Tame Graphs.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2006

An operational semantics and type safety prooffor multiple inheritance in C++.

[BibT_eX]

[DOI]

Proceedings of the 21th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2006

Verifying a Hotel Key Card System.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2006

Flyspeck I: Tame Graphs.

[BibT_eX]

[DOI]

Paula Schultz

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

Proving pointer programs in higher-order logic.

[BibT_eX]

[DOI]

Farhad Mehta

Inf. Comput., 2005

Bytecode Analysis for Proof Carrying Code.

[BibT_eX]

[DOI]

Martin Wildmoser

Amine Chaieb

Proceedings of the First Workshop on Bytecode Semantics, 2005

Jinja is not Java.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2005

Proof Pearl: Defining Functions over Finite Sets.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic.

[BibT_eX]

[DOI]

Amine Chaieb

Proceedings of the Logic for Programming, 2005

Asserting Bytecode Safety.

[BibT_eX]

[DOI]

Martin Wildmoser

Proceedings of the Programming Languages and Systems, 2005

Towards a Verified Enumeration of All Tame Plane Graphs.

[BibT_eX]

[DOI]

Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005

2004

AVL Trees.

[BibT_eX]

[DOI]

Cornelia Pusch

Arch. Formal Proofs, 2004

Compiling Exceptions Correctly.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2004

Functional Automata.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2004

Mini ML.

[BibT_eX]

[DOI]

Wolfgang Naraschewski

Arch. Formal Proofs, 2004

Certifying Machine Code Safety: Shallow Versus Deep Embedding.

[BibT_eX]

[DOI]

Martin Wildmoser

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

Random Testing in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

Prototyping Proof Carrying Code.

[BibT_eX]

[DOI]

Proceedings of the Exploring New Frontiers of Theoretical Informatics, 2004

2003

Verified bytecode verifiers.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2003

Java Bytecode Verification.

[BibT_eX]

[DOI]

J. Autom. Reason., 2003

2002

Structured Proofs in Isar/HOL.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, Second International Workshop, 2002

The 5 Colour Theorem in Isabelle/Isar.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited.

[BibT_eX]

[DOI]

David von Oheimb

Proceedings of the FME 2002: Formal Methods, 2002

Hoare Logics for Recursive Procedures and Unbounded Nondeterminism.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 16th International Workshop, 2002

Isabelle/HOL - A Proof Assistant for Higher-Order Logic

[BibT_eX]

[DOI]

Markus Wenzel

Lecture Notes in Computer Science 2283, Springer, ISBN: 3-540-43376-7, 2002

2001

More Church-Rosser Proofs.

[BibT_eX]

[DOI]

J. Autom. Reason., 2001

Verified lightweight bytecode verification.

[BibT_eX]

[DOI]

Concurr. Comput. Pract. Exp., 2001

Verified Bytecode Verifiers.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2001

2000

Preface.

[BibT_eX]

[DOI]

Inf. Comput., 2000

Executing Higher Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Workshop, 2000

Proof Terms for Simply Typed Higher Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

Workshop über Rigorose Entwicklung software-intensiver Systeme.

[BibT_eX]

[DOI]

Proceedings of the Informatik 2000, 2000

1999

HOLCF=HOL+LCF.

[BibT_eX]

[DOI]

J. Funct. Program., 1999

Type Inference Verified: Algorithm W in Isabelle/HOL.

[BibT_eX]

[DOI]

Wolfgang Naraschewski

J. Autom. Reason., 1999

Machine-Checking the Java Specification: Proving Type-Safety.

[BibT_eX]

[DOI]

David von Oheimb

Proceedings of the Formal Syntax and Semantics of Java, 1999

Owicki/Gries in Isabelle/HOL.

[BibT_eX]

[DOI]

Leonor Prensa Nieto

Proceedings of the Fundamental Approaches to Software Engineering, 1999

Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract).

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1999

1998

Higher-Order Rewrite Systems and Their Confluence.

[BibT_eX]

[DOI]

Richard Mayr

Theor. Comput. Sci., 1998

Winskel is (almost) Right: Towards a Mechanized Semantics.

[BibT_eX]

[DOI]

Formal Aspects Comput., 1998

Verified Lexical Analysis.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 11th International Conference, 1998

Javalight is Type-Safe - Definitely.

[BibT_eX]

[DOI]

David von Oheimb

Proceedings of the POPL '98, 1998

Term rewriting and all that.

[BibT_eX]

Franz Baader

Cambridge University Press, ISBN: 978-0-521-45520-6, 1998

1997

Traces of I/O-Automata in Isabelle/HOLCF.

[BibT_eX]

[DOI]

Olaf Müller

Proceedings of the TAPSOFT'97: Theory and Practice of Software Development, 1997

1996

Formal Verification of Algorithm W: The Monomorphic Case.

[BibT_eX]

[DOI]

Dieter Nazareth

Proceedings of the Theorem Proving in Higher Order Logics, 9th International Conference, 1996

Winskel is (Almost) Right: Towards a Mechanized Semantics Textbook.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1996

More Church-Rosser Proofs (in Isabelle/HOL).

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995

Type Reconstruction for Type Classes.

[BibT_eX]

[DOI]

Christian Prehofer

J. Funct. Program., 1995

Combining Model Checking and Deduction for I/O-Automata.

[BibT_eX]

[DOI]

Olaf Müller

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1995

Higher-Order Rewrite Systems (Abstract).

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 6th International Conference, 1995

1994

Reduction and Unification in Lambda Calculi with a General Notion of Subtype.

[BibT_eX]

[DOI]

Zhenyu Qian

J. Autom. Reason., 1994

I/Q Automata in Isabelle/HOL.

[BibT_eX]

[DOI]

Konrad Slind

Proceedings of the Types for Proofs and Programs, 1994

Interpreter Verification for a Functional Language.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1994

1993

Orthogonal Higher-Order Rewrite Systems are Confluent.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 1993

Type Checking Type Classes.

[BibT_eX]

[DOI]

Christian Prehofer

Proceedings of the Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1993

Functional Unification of Higher-Order Patterns

[BibT_eX]

[DOI]

Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), 1993

1992

Reduction and Unification in Lambda Calculi with Subtypes.

[BibT_eX]

[DOI]

Zhenyu Qian

Proceedings of the Automated Deduction, 1992

Isabelle-91.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1992

1991

Combining Matching Algorithms: The Regular Case.

[BibT_eX]

[DOI]

J. Symb. Comput., 1991

Constructive Rewriting.

[BibT_eX]

[DOI]

Comput. J., 1991

Modular Higher-Order E-Unification.

[BibT_eX]

[DOI]

Zhenyu Qian

Proceedings of the Rewriting Techniques and Applications, 4th International Conference, 1991

Higher-Order Critical Pairs

[BibT_eX]

[DOI]

Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), 1991

Type Classes and Overloading Resolution via Order-Sorted Unification.

[BibT_eX]

[DOI]

Gregor Snelting

Proceedings of the Functional Programming Languages and Computer Architecture, 1991

1990

Unification in Primal Algebras, Their Powers and Their Varieties

[BibT_eX]

[DOI]

J. ACM, October, 1990

Proof Transformations for Equational Theories

[BibT_eX]

[DOI]

Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990

Automating Squiggol.

[BibT_eX]

Proceedings of the Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 1990

Higher-Order Unification, Polymorphism, and Subsorts (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Conditional and Typed Rewriting Systems, 1990

Ordered Rewriting and Confluence.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Automated Deduction, 1990

1989

Equational Reasoning in Isabelle.

[BibT_eX]

[DOI]

Sci. Comput. Program., 1989

Boolean Unification - The Story So Far.

[BibT_eX]

[DOI]

J. Symb. Comput., 1989

Term Rewriting and Beyond - Theorem Proving in Isabelle.

[BibT_eX]

[DOI]

Formal Aspects Comput., 1989

Combining Matching Algorithms: The Rectangular Case.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989

Formal Verification of Data Type Refinement - Theory and Practice.

[BibT_eX]

[DOI]

Proceedings of the Stepwise Refinement of Distributed Systems, 1989

1988

Unification in Boolean Rings.

[BibT_eX]

[DOI]

J. Autom. Reason., 1988

Unification in Primal Algebras.

[BibT_eX]

[DOI]

Proceedings of the CAAP '88, 1988

1987

Are Homomorphisms Sufficient for Behavioural Implementations of Deterministic and Nondeterministic Data Types?

[BibT_eX]

[DOI]

Proceedings of the STACS 87, 1987

Observing Non-Deterministic Data Types.

[BibT_eX]

[DOI]

Proceedings of the Recent Trends in Data Type Specification, 1987

1986

Behavioural implementation concepts for nondeterministic data types.

[BibT_eX]

[DOI]

PhD thesis, 1986

Non-deterministic Data Types: Models and Implementations.

[BibT_eX]

[DOI]

Acta Informatica, 1986

Behavioural Implementations of Non-Deterministic Data Types.

[BibT_eX]

Proceedings of the 4st Workshop on Abstract Data Type, 1986

1983

A decidability result about sufficient-completeness of axiomatically specified abstract data types.

[BibT_eX]

[DOI]