Logics and Type Systems in Theory and Practice

Name: Logics and Type Systems in Theory and Practice | Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday
Brand: Springer
Price: 128.39 EUR
Availability: OnlineOnly

Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday

Venanzio Capretta Robbert Krebbers Freek Wiedijk(Herausgeber*in)

Springer (Verlag)

Erschienen am 21. Mai 2024

XII, 273 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-031-61716-4 (ISBN)

128,39 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Preface
List of Expert Reviewers
Contents
Sequential Value Passing Yields a Kleene Theorem for Processes
1 Introduction
2 Preliminaries
3 Regular Expressions
4 Signals and Conditions
5 Sequencing
6 Pushdown Processes
7 Conclusion
References
YACC: Yet Another Church Calculus
1 Introduction
2 Syntax of TIC
3 Type Reconstruction
4 Operational Semantics of TIC
5 Relations with Intersection Type Assignment Systems
6 Related Works and Conclusion
References
Safe Smooth Paths Between Straight Line Obstacles
1 Introduction
2 A Combination of Algorithms
3 Producing a Sequence of Events
4 Producing Cells
5 Making a Broken Line Trajectory Between Two Points
6 Making a Smooth Trajectory
7 Exploiting the Program and Visual Feedback
8 Future Work
9 Related Work
10 Conclusion
References
Learning Guided Automated Reasoning: A Brief Survey
1 Introduction
2 Early History
3 Characterization of Mathematical Knowledge
3.1 Syntactic Features
3.2 ENIGMA Syntactic Features
3.3 More Semantic Features
3.4 Characterization Using Neural Networks
4 Premise Selection
4.1 k-Nearest Neighbors (k-NN)
4.2 Naive Bayes
4.3 Decision Trees
4.4 Neural Methods
5 Guidance of Saturation-Based ATPs
6 Guidance of Tableaux and Instantiation-Based ATPs
7 Tactic Based ITP Guidance
7.1 Overview
7.2 Advantages of Tactic-Based ITP Guidance
7.3 Challenges in Tactic-Based ITP Guidance
8 Related Symbolic Classification Problems
9 Conclusion
References
Approximation Fixpoint Theory in Coq
1 Introduction
2 Ordinals and Lattices
3 Approximators and Fixpoints
4 An Example: Propositional Logic Programming
5 Related Work
6 Conclusions
References
Constructing Morphisms for Arithmetic Subsequences of Fibonacci
1 Introduction
2 Preliminaries and Main Result
3 Fibonacci Numbers
4 Fibonacci Morphism
5 Proof of the Theorem
6 Examples
7 Further Remarks
References
A Variation of Reynolds-Hurkens Paradox
1 Introduction
2 Some Paradoxes in Minimal Higher-Order Logic
2.1 A Variation of Russell's Paradox
2.2 A Refinement
3 An Encoding in U-
3.1 Weak Representation of Data Type
3.2 Some Variations
4 Computational Behavior
4.1 Family of Looping Combinators
4.2 Definitions and Head Linear Reduction
5 Conclusion
References
Between Brackets
1 Introduction
1.1 Constants Between Matching Brackets
1.2 Matching Brackets Between Constants
1.3 Two Brackets Between Constants
2 Strings and Terms
3 Context-Free Languages Representing Terms
3.1 Languages for Terms
3.2 Notations
3.3 Polish Notations
4 Circular Embedded Trees
4.1 Dual Structure
4.2 Dual and Weak Dual Graphs
4.3 Squaregraphs
5 Conclusion
References
Some Probabilistic Riddles and Some Logical Solutions
1 Introduction
2 Preliminaries
3 Hard Conditional Probability Problem
4 Probability of Second Girl Child
5 Tricky Probability Interview Puzzle
6 Life or Death
7 Paradox Probability Puzzle
8 Tricky Problem on Probability
References
It's All a Game
1 Introduction
2 Preliminaries
2.1 Bisimulation Games
2.2 Apartness
3 From Bisimulation Games to Apartness and Back
3.1 Spoiler-Strategies Constructed from Apartness Proofs
3.2 Spoiler-Strategy Induced Deductive Proofs of Apartness
4 Conclusions and Future Work
References
Multisets and Distributions
1 Introduction
2 The Distribution and Multiset Monads
3 Lists and Distributions
3.1 A Distributive Law L:LFFL
3.2 The Parikh Map #:LM
3.3 A Distributive Law M:MFFM
4 A General Result
5 Conclusion
A Extra Proofs
A.1 L:LFFL Is a Distributive Law
A.2 Conditions of Theorem 3
References
Minimal Depth Distinguishing Formulas Without Until for Branching Bisimulation
1 Introduction
2 Preliminaries
3 A Hennessy-Milner Theorem
4 Computing Minimal Depth Distinguishing Formulas
4.1 Implementation Details and Example
References
Relating Apartness and Branching Bisimulation Games
1 Introduction
2 Strong Bisimilarity
3 Branching Bisimilarity
4 Future Work
References
Fixed Point Theorems in Computability Theory
1 Introduction
2 The Second Recursion Theorem
3 Partial Combinatory Algebra
4 The Theory of Numberings
5 Overview
6 Fixed Point Free Functions and Arslanov's Completeness Criterion
7 Further Generalizations
8 Effectiveness and Other Remarks
References
A New Perspective on Conformance Testing Based on Apartness
1 Introduction
2 Partial Mealy Machines and Apartness
3 Main Result
4 Deriving Previous k-Completeness Results
5 Conclusions and Future Work
References
The Interval Domain in Homotopy Type Theory
1 Introduction
2 Preliminaries on Domain Theory
2.1 (Continuous) DCPOs
2.2 Scott Topology and Apartness
2.3 Strongly Maximal Elements
3 The Interval Domain
4 Strong Maximality and Locatedness
5 Real Arithmetic
6 Arithmetic Laws
7 Conclusions and Related Work
References
Characterizing Morphic Sequences
1 Introduction
2 Notation and Preliminaries
3 Tree Structures of Morphic Sequences
4 Morphic Sequences Characterized by Automata
5 Morphic Sequences Characterized by Subsequences
6 Morphic Sequences Characterized by Rational Infinite Terms
7 Morphic Sequences Characterized by Infinitary Rewriting
8 Conclusions
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken