This thesis is a contribution to Solomon Feferman's Unfolding Program which aims to provide a general method of capturing the operations on individuals and predicates (and the principles governing them) that are implicit in a formal axiomatic system based on open-ended schemata. The thesis in particular studies the unfolding of the classical system for one generalized positive arithmetical inductive definition. The main result is an ordinal analysis of this theory. The resulting ordinal has been known since Heinz Bachmann, and has been studied by Peter Aczel, who felt it should be of proof-theoretic interest. Solomon Feferman conjectured specifically that it should be the strength of the theory under consideration here, and this thesis verifies his conjecture. The upper bound proceeds via a system of numbers, inductive definitions and ordinals that is analyzed with a combination of operator-controlled derivations and asymmetric interpretation. The lower bound is established through a well-ordering proof that uses the unfolding machinery to construct hierarchies based on jump operators. This part highlights a new ingredient needed in the unfolding at this level, namely a dependent version of the join operator, producing disjoint unions of predicates indexed by a predicate. The thesis also includes an appendix detailing the history and motivation of the unfolding program, as well as an appendix describing previous work on the Aczel-Bachmann ordinal.
14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21 - 23, 2016, Proceedings
Author: Atsushi Igarashi
This book constitutes the refereed proceedings of the 14th Asian Symposium on Programming Languages and Systems, APLAS 2016, held in Hanoi, Vietnam, in November 2016. The papers cover a variety of topics such as semantics, logics, and foundational theory; design of languages type systems, and foundational calculi; domain-specific languages; compilers, interpreters, and abstract machines; program derivation, synthesis and transformation; program analysis, verification, and model-checking; logic, constraint, probabilistic and quantum programming; software security; concurrency and parallelism; tools for programming and implementation.
This volume honours the life and work of Solomon Feferman, one of the most prominent mathematical logicians of the latter half of the 20th century. In the collection of essays presented here, researchers examine Feferman’s work on mathematical as well as specific methodological and philosophical issues that tie into mathematics. Feferman’s work was largely based in mathematical logic (namely model theory, set theory, proof theory and computability theory), but also branched out into methodological and philosophical issues, making it well known beyond the borders of the mathematics community. With regard to methodological issues, Feferman supported concrete projects. On the one hand, these projects calibrate the proof theoretic strength of subsystems of analysis and set theory and provide ways of overcoming the limitations imposed by Gödel’s incompleteness theorems through appropriate conceptual expansions. On the other, they seek to identify novel axiomatic foundations for mathematical practice, truth theories, and category theory. In his philosophical research, Feferman explored questions such as “What is logic?” and proposed particular positions regarding the foundations of mathematics including, for example, his “conceptual structuralism.” The contributing authors of the volume examine all of the above issues. Their papers are accompanied by an autobiography presented by Feferman that reflects on the evolution and intellectual contexts of his work. The contributing authors critically examine Feferman’s work and, in part, actively expand on his concrete mathematical projects. The volume illuminates Feferman’s distinctive work and, in the process, provides an enlightening perspective on the foundations of mathematics and logic.
8th International Conference, TACAS 2002, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002. Proceedings
Author: Joost-Pieter Katoen
ETAPS 2002 was the ?fth instance of the European Joint Conferences on Theory and Practice of Software. ETAPS is an annual federated conference that was established in 1998by combining a number of existing and new conferences. This year it comprised 5 conferences (FOSSACS, FASE, ESOP, CC, TACAS), 13 satellite workshops (ACL2, AGT, CMCS, COCV, DCC, INT, LDTA, SC, SFEDL, SLAP, SPIN, TPTS, and VISS), 8invited lectures (not including those speci?c to the satellite events), and several tutorials. The events that comprise ETAPS address various aspects of the system - velopment process, including speci?cation, design, implementation, analysis, and improvement. The languages, methodologies, and tools which support these - tivities are all well within its scope. Di?erent blends of theory and practice are represented, with an inclination towards theory with a practical motivation on one hand and soundly-based practice on the other. Many of the issues involved in software design apply to systems in general, including hardware systems, and the emphasis on software is not intended to be exclusive.
20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008, Proceedings
Author: Aarti Gupta
Publisher: Springer Science & Business Media
This volume contains the proceedings of the 20th International Conference on Computer Aided Veri?cation (CAV) held in Princeton, New Jersey, USA, d- ing July 7–14, 2008. CAV is dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. Its scope ranges from theoretical results to concrete applications, with an emphasis on practical veri?cation tools and the underlying algorithms and techniques. Overall, 2008 has been a historical year for CAV. – It marks the 20th anniversaryof CAV, which has servedas a forum for ideas whose impact is now clearly felt in research and practice. – It celebrates the recognitionreceived by Edmund M. Clarke, E. Allen Em- son and Joseph Sifakis as winners of the 2007 ACM Turing Award for their researchin model checking.CAV is proudto have been the intellectual home for model checking over these 20 years. – Inrecognitionofthelargebodyofcontributionsmadetothe?eldofcomput- aidedveri?cation,theCAVAwardwasinstitutedthisyearwiththe?rstw- ner announcedatthe conference,andacitationto appear inthe proceedings of the 21st CAV. There were 131 paper submissions, divided into 104 regular and 27 tool - pers. These went through an active review process, with each submission - viewed by at least 3, and on average4, members of the ProgramCommittee. We also sought external reviews from experts in certain areas. Authors had the - portunity to respond to the initial reviews during an author response period. All these inputs were used by the Program Committee in selecting a ?nal program with 33 regular papers and 14 tool papers.