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 focusingannotations 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
inria.fr
Author only
