Result page:
**1**
2
3
4
5

1

Proof checking and logic programming

July 2015
PPDP '15: Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming

**Publisher:** ACM

**Bibliometrics**:

Citation Count: 0

Downloads (6 Weeks): 1, Downloads (12 Months): 15, Downloads (Overall): 15

Full text available:

PDF

In a world where trusting software systems is problematic, formal methods and formal proofs should be able to help. Proof checking can play an important role in establishing trust since such checkers can be smaller and easier to verify than, for example, entire theorem provers or model checkers. Proof checking ...

**Keywords**:
focused proof systems, proof checking, foundational proof certificates

2

A Lightweight Formalization of the Metatheory of Bisimulation-Up-To

January 2015
CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

**Publisher:** ACM

**Bibliometrics**:

Citation Count: 0

Downloads (6 Weeks): 2, Downloads (12 Months): 25, Downloads (Overall): 25

Full text available:

PDF

Bisimilarity of two processes is formally established by producing a bisimulation relation that contains those two processes and obeys certain closure properties. In many situations, particularly when the underlying labeled transition system is unbounded, these bisimulation relations can be large and even infinite. The bisimulation-up-to technique has been developed to ...

**Keywords**:
process calculus, abella, λ-tree syntax, bisimulation-up-to, co-induction

3

Foundational proof certificates: making proof universal and permanent

September 2013
LFMTP '13: Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice

**Publisher:** ACM

**Bibliometrics**:

Citation Count: 0

Downloads (6 Weeks): 1, Downloads (12 Months): 5, Downloads (Overall): 17

Full text available:

PDF

Consider a world where exporting proof evidence into a declarative, universal, and permanent format is taken as ``feature zero'' for computational logic systems. In such a world, provers will be able to communicate and share theorems and proofs; libraries can archive and organize proofs; and marketplaces of proofs would be ...

**Keywords**:
proof certificates, focused proof systems

4

A formal framework for specifying sequent calculus proof systems

January 2013
Theoretical Computer Science: Volume 474, February, 2013

**Publisher:** Elsevier Science Publishers Ltd.

Intuitionistic logic and intuitionistic type systems are commonly used as frameworks for the specification of natural deduction proof systems. In this paper we show how to use classical linear logic as a logical framework to specify sequent calculus proof systems and to establish some simple consequences of the specified sequent ...

**Keywords**:
Linear logic, Cut elimination, Logical frameworks, Sequent calculus, Proof systems

5

A Two-Level Logic Approach to Reasoning About Computations

July 2012
Journal of Automated Reasoning: Volume 49 Issue 2, August 2012

**Publisher:** Springer-Verlag New York, Inc.

Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, typing, and acceptance by non-deterministic machines. We therefore propose a (restricted) logical theory over relations as a language for specifying such notions. Our specification logic is further characterized by an ability to explicitly treat binding ...

**Keywords**:
∇-quantification, Two-level logic, λ-tree syntax, Generic judgments, Nominal abstraction

6

Programming with Higher-Order Logic

June 2012

Formal systems that describe computations over syntactic structures occur frequently in computer science. Logic programming provides a natural framework for encoding and animating such systems. However, these systems often embody variable binding, a notion that must be treated carefully at a computational level. This book aims to show that a ...

7

A proposal for broad spectrum proof certificates

December 2011
CPP'11: Proceedings of the First international conference on Certified Programs and Proofs

**Publisher:** Springer-Verlag

Recent developments in the theory of focused proof systems provide flexible means for structuring proofs within the sequent calculus. This structuring is organized around the construction of “macro” level inference rules based on the “micro” inference rules which introduce single logical connectives. After presenting focused proof systems for first-order classical ...

8

Nominal abstraction

December 2010
Information and Computation: Volume 209 Issue 1, January, 2011

**Publisher:** Academic Press, Inc.

Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such descriptions: the interpretation of atomic judgments through recursive definitions and an encoding of binding constructs via generic judgments. However, logics ...

**Keywords**:
λ-Tree syntax, Proof search, Reasoning about operational semantics, Generic judgments, Higher-order abstract syntax

9

Reasoning about computations using two-levels of logic

November 2010
APLAS'10: Proceedings of the 8th Asian conference on Programming languages and systems

**Publisher:** Springer-Verlag

We describe an approach to using one logic to reason about specifications written in a second logic. One level of logic, called the "reasoning logic", is used to state theorems about computational specifications. This logic is classical or intuitionistic and should contain strong proof principles such as induction and co-induction. ...

10

A Framework for Proof Systems

July 2010
Journal of Automated Reasoning: Volume 45 Issue 2, August 2010

**Publisher:** Springer-Verlag New York, Inc.

Linear logic can be used as a meta-logic to specify a range of object-level proof systems. In particular, we show that by providing different polarizations within a focused proof system for linear logic, one can account for natural deduction (normal and non-normal), sequent proofs (with and without cut), and tableaux ...

**Keywords**:
Meta-logic, Linear logic, Logical framework, Focusing

11

Focused inductive theorem proving

July 2010
IJCAR'10: Proceedings of the 5th international conference on Automated Reasoning

**Publisher:** Springer-Verlag

Focused proof systems provide means for reducing and structuring the non-determinism involved in searching for sequent calculus proofs. We present a focused proof system for a first-order logic with inductive and co-inductive definitions in which the introduction rules are partitioned into an asynchronous phase and a synchronous phase. These focused ...

12

Finding unity in computational logic

April 2010
ACM-BCS '10: Proceedings of the 2010 ACM-BCS Visions of Computer Science Conference

**Publisher:** British Computer Society

**Bibliometrics**:

Citation Count: 1

Downloads (6 Weeks): 4, Downloads (12 Months): 13, Downloads (Overall): 88

Full text available:

PDF

While logic was once developed to serve philosophers and mathematicians, it is increasingly serving the varied needs of computer scientists. In fact, recent decades have witnessed the creation of the new discipline of Computational Logic. While Computation Logic can claim involvement in diverse areas of computing, little has been done ...

**Keywords**:
proof theory, unity of logic, computational logic, sequent calculus, focused proof systems

13

Proof search specifications of bisimulation and modal logics for the π-calculus

January 2010
ACM Transactions on Computational Logic (TOCL): Volume 11 Issue 2, January 2010

**Publisher:** ACM

**Bibliometrics**:

Citation Count: 5

Downloads (6 Weeks): 4, Downloads (12 Months): 20, Downloads (Overall): 239

Full text available:

PDF

We specify the operational semantics and bisimulation relations for the finite π-calculus within a logic that contains the ∇ quantifier for encoding generic judgments and definitions for encoding fixed points. Since we restrict to the finite case, the ability of the logic to unfold fixed points allows this logic to ...

**Keywords**:
bisimulation, modal logics, ∇ quantifier, generic judgments, Proof search, higher-order abstract syntax, λ-tree syntax, π-calculus

14

Focusing and polarization in linear, intuitionistic, and classical logics

October 2009
Theoretical Computer Science: Volume 410 Issue 46, November, 2009

**Publisher:** Elsevier Science Publishers Ltd.

A focused proof system provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured. Within linear logic, the focused proof system of Andreoli provides an elegant and comprehensive normal form for cut-free proofs. Within intuitionistic and classical logics, there are various ...

**Keywords**:
Classical logic, Focused proof system, Sequent calculus, Intuitionistic logic

15

Algorithmic specifications in linear logic with subexponentials

September 2009
PPDP '09: Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming

**Publisher:** ACM

**Bibliometrics**:

Citation Count: 12

Downloads (6 Weeks): 0, Downloads (12 Months): 12, Downloads (Overall): 93

Full text available:

PDF

The linear logic exponentials !,? are not canonical: one can add to linear logic other such operators, say ! l ,? 1 , which may or may not allow contraction and weakening, and where l is from some pre-ordered set of labels. We shall call these additional operators subexponentials and ...

**Keywords**:
proof search, linear logic, subexponentials

16

A Unified Sequent Calculus for Focused Proofs

August 2009
LICS '09: Proceedings of the 2009 24th Annual IEEE Symposium on Logic In Computer Science

**Publisher:** IEEE Computer Society

We present a compact sequent calculus LKU for classical logic organized around the concept of polarization. Focused sequent calculi for classical logic, intuitionistic logic, and multiplicative-additive linear logic are derived as fragments of LKU by increasing the sensitivity of specialized structural rules to polarity information. We develop a unified, streamlined ...

**Keywords**:
Proof theory, focused proof systems, linear logic

17

Formalizing Operational Semantic Specifications in Logic

July 2009
Electronic Notes in Theoretical Computer Science (ENTCS): Volume 246, August, 2009

**Publisher:** Elsevier Science Publishers B. V.

We review links between three logic formalisms and three approaches to specifying operational semantics. In particular, we show that specifications written with (small-step and big-step) SOS, abstract machines, and multiset rewriting, are closely related to Horn clauses, binary clauses, and (a subset of) linear logic, respectively. We shall illustrate how ...

**Keywords**:
big-step SOS semantics, Operational semantics, multiset rewriting, small-step SOS semantics, specifications

18

Reasoning in Abella about Structural Operational Semantics Specifications

December 2008
Electronic Notes in Theoretical Computer Science (ENTCS): Volume 228, January, 2009

**Publisher:** Elsevier Science Publishers B. V.

The approach to reasoning about structural operational semantics style specifications supported by the Abella system is discussed. This approach uses @l-tree syntax to treat object language binding and encodes binding related properties in generic judgments. Further, object language specifications are embedded directly into the reasoning framework through recursive definitions. The ...

**Keywords**:
λ-tree syntax, Abella, object language binding, Structural operational semantics

19

Focusing in Linear Meta-logic

August 2008
IJCAR '08: Proceedings of the 4th international joint conference on Automated Reasoning

**Publisher:** Springer-Verlag

It is well known how to use an intuitionistic meta-logic to specify natural deduction systems. It is also possible to use linear logic as a meta-logic for the specification of a variety of sequent calculus proof systems. Here, we show that if we adopt different *focusing*annotations for such linear logic ...

20

A Neutral Approach to Proof and Refutation in MALL

June 2008
LICS '08: Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science

**Publisher:** IEEE Computer Society

We propose a setting in which the search for a proof of B or a refutation of B (a proof of not B) can be carried out simultaneously. In contrast with the usual approach in automated deduction, we do not need to first commit to either proving B or to ...

**Keywords**:
neutral approach, linear logic, game semantics