Marc Bezem

Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, 2024

2022

Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2022

Type Theories with Universe Level Judgements.

[BibT_eX]

[DOI]

CoRR, 2022

Type Theory with Explicit Universe Polymorphism.

[BibT_eX]

[DOI]

Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

2021

On generalized algebraic theories and categories with families.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2021

2020

A Note on Generalized Algebraic Theories and Categories with Families.

[BibT_eX]

[DOI]

CoRR, 2020

2019

The Univalence Axiom in Cubical Sets.

[BibT_eX]

[DOI]

Simon Huber

J. Autom. Reason., 2019

Skolem's Theorem in Coherent Logic.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2019

Construction of the Circle in UniMath.

[BibT_eX]

[DOI]

Ulrik Buchholtz

Daniel R. Grayson

CoRR, 2019

2016

A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic.

[BibT_eX]

[DOI]

Robin Adams

CoRR, 2016

Improving IntSat by expressing disjunctions of bounds as linear constraints.

[BibT_eX]

[DOI]

Roberto Asín

AI Commun., 2016

Realizability at Work: Separating Two Constructive Notions of Finiteness.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic.

[BibT_eX]

[DOI]

Robin Adams

Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

2015

A Kripke model for simplicial sets.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2015

Non-Constructivity in Kan Simplicial Sets.

[BibT_eX]

[DOI]

Erik Parmann

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

2014

A Vernacular for Coherent Logic.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

2013

A Model of Type Theory in Cubical Sets.

[BibT_eX]

[DOI]

Simon Huber

Proceedings of the 19th International Conference on Types for Proofs and Programs, 2013

2012

A type system for counting instances of software components.

[BibT_eX]

[DOI]

Dag Hovland

Hoang Truong

Theor. Comput. Sci., 2012

On streams that are finitely red

[BibT_eX]

[DOI]

Keiko Nakata

Tarmo Uustalu

Log. Methods Comput. Sci., 2012

Expressive power of digraph solvability.

[BibT_eX]

[DOI]

Clemens Grabmayer

Michal Walicki

Ann. Pure Appl. Log., 2012

2011

A Proof Pearl with the Fan Theorem and Bar Induction - Walking through Infinite Trees with Mixed Induction and Coinduction.

[BibT_eX]

[DOI]

Keiko Nakata

Tarmo Uustalu

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

2010

Hard problems in max-algebra, control theory, hypergraphs and other areas.

[BibT_eX]

[DOI]

Enric Rodríguez-Carbonell

Inf. Process. Lett., 2010

2009

Developing Bounded Reasoning.

[BibT_eX]

[DOI]

Michal Walicki

Wojtek Szajnkenig

J. Log. Lang. Inf., 2009

Skolem Machines.

[BibT_eX]

[DOI]

John Fisher

Fundam. Informaticae, 2009

2008

On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic.

[BibT_eX]

[DOI]

Dimitri Hendriks

J. Autom. Reason., 2008

Exponential behaviour of the Butkovic-Zimmermann algorithm for solving two-sided linear systems in max-algebra.

[BibT_eX]

[DOI]

Enric Rodríguez-Carbonell

Discret. Appl. Math., 2008

The Max-Atom Problem and Its Relevance.

[BibT_eX]

[DOI]

Enric Rodríguez-Carbonell

Proceedings of the Logic for Programming, 2008

2007

Query Completeness of Skolem Machine Computations.

[BibT_eX]

[DOI]

John Fisher

Proceedings of the Machines, Computations, and Universality, 5th International Conference, 2007

Completeness and Decidability in Sequence Logic.

[BibT_eX]

[DOI]

Tore Langholm

Michal Walicki

Proceedings of the Logic for Programming, 2007

Skolem Machines and Geometric Logic.

[BibT_eX]

[DOI]

John Fisher

Proceedings of the Theoretical Aspects of Computing, 2007

2005

Automating Coherent Logic.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2005

Finding Resource Bounds in the Presence of Explicit Deallocation.

[BibT_eX]

[DOI]

Hoang Truong

Proceedings of the Theoretical Aspects of Computing, 2005

On the Undecidability of Coherent Logic.

[BibT_eX]

[DOI]

Proceedings of the Processes, 2005

2004

Black Box and White Box Identification of Formal Languages Using Test Sets.

[BibT_eX]

[DOI]

Christian Sloper

Tore Langholm

Grammars, 2004

2003

A Descriptive Characterisation of Even Linear Languages.

[BibT_eX]

[DOI]

Tore Langholm

Grammars, 2003

A Type System for the Safe Instantiation of Components.

[BibT_eX]

[DOI]

Hoang Truong

Proceedings of FOCLASA 2003, 2003

Newman's lemma - a case study in proof automation and geometric logic, Logic in Computer Science Column.

[BibT_eX]

Bull. EATCS, 2003

2002

Automated Proof Construction in Type Theory Using Resolution.

[BibT_eX]

[DOI]

Dimitri Hendriks

Hans de Nivelle

J. Autom. Reason., 2002

2001

An Improved Extensionality Criterion for Higher-Order Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 15th International Workshop, 2001

1999

Extensionality of Simply Typed Logic Programs.

[BibT_eX]

Proceedings of the Logic Programming: The 1999 International Conference, Las Cruces, New Mexico, USA, November 29, 1999

Formulas as Programs.

[BibT_eX]

[DOI]

Krzysztof R. Apt

Proceedings of the Logic Programming Paradigm - A 25-Year Perspective, 1999

1998

On the Computational Content of the Axiom of Choice.

[BibT_eX]

[DOI]

Stefano Berardi

J. Symb. Log., 1998

Diagram Techniques for Confluence.

[BibT_eX]

[DOI]

Jan Willem Klop

Vincent van Oostrom

Inf. Comput., 1998

Formulas as Programs

[BibT_eX]

[DOI]

Krzysztof R. Apt

CoRR, 1998

1997

Two Finite Specifications of a Queue.

[BibT_eX]

[DOI]

Alban Ponse

Theor. Comput. Sci., 1997

Formalizing Process Algebraic Verifications in the Calculus of Constructions.

[BibT_eX]

[DOI]

Roland N. Bol

Jan Friso Groote

Formal Aspects Comput., 1997

1996

A Simple Proof of the Undecidability of Inhabitation in lambda<i>P</i>.

[BibT_eX]

[DOI]

Jan Springintveld

J. Funct. Program., 1996

Polymorphic Extensions of Simple Type Structures - With an Application to Bar Recursive Minimization.

[BibT_eX]

[DOI]

Erik Barendsen

Ann. Pure Appl. Log., 1996

1995

A realization of the negative interpretation of the Axiom of Choice.

[BibT_eX]

[DOI]

Stefano Berardi

Proceedings of the Typed Lambda Calculi and Applications, 1995

1994

Undecidable Goals for Completed Acyclic Programs.

[BibT_eX]

[DOI]

Jan Keuzenkamp

New Gener. Comput., 1994

A Correctness Proof of a One-Bit Sliding Window Protocol in µCRL.

[BibT_eX]

[DOI]

Jan Friso Groote

Comput. J., 1994

Invariants in Process Algebra with Data.

[BibT_eX]

[DOI]

Jan Friso Groote

Proceedings of the CONCUR '94, 1994

1993

Strong Termination of Logic Programs.

[BibT_eX]

[DOI]

J. Log. Program., 1993

1991

Acyclic Programs.

[BibT_eX]

[DOI]

Krzysztof R. Apt

New Gener. Comput., 1991

Semantics and Consistency of Rule-Based Expert Systems.

[BibT_eX]

[DOI]

J. Log. Comput., 1991

1990

Completeness of Resolution Revisited.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1990

1989

Compact and Majorizable Functionals of Finite Type.

[BibT_eX]

[DOI]

J. Symb. Log., 1989

Characterizing Termination of Logic Programs with Level Mappings.

[BibT_eX]

Proceedings of the Logic Programming, 1989

1988

On Estimating the Complexity of Logarithmic Decompositions.

[BibT_eX]

[DOI]

Jan van Leeuwen

Inf. Process. Lett., 1988

Equivalence of bar recursors in the theory of functionals of finite type.

[BibT_eX]

[DOI]

Arch. Math. Log., 1988

Consistency of Rule-based Expert System.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Automated Deduction, 1988

1985

Strongly Majorizable Functionals of Finite Type: A Model for Barrecursion Containing Discontinuous Functionals.

[BibT_eX]

[DOI]

J. Symb. Log., 1985

Isomorphisms Between HEO and HROE, ECF and ICFE.

[BibT_eX]

[DOI]

J. Symb. Log., 1985

Strong normalization of barrecursive terms without using infinite terms.

[BibT_eX]

[DOI]