000			06747cam a2200649 i 4500
001			on1435881220
003			OCoLC
005			20250707095601.0
006			m o d
007			cr cnu|||unuuu
008			240528s2024 sz a o 011 0 eng d
040			_aGW5XE _beng _erda _epn _cGW5XE _dOCLCO _dEBLCP _dEMRUN _dOCLCO _dOCLCQ
019			_a1435750352
020			_a9783031617164 _q(electronic bk.)
020			_a3031617169 _q(electronic bk.)
020			_z9783031617157
024	7		_a10.1007/978-3-031-61716-4 _2doi
035			_a(OCoLC)1435881220 _z(OCoLC)1435750352
050		4	_aQA76.9.L63
072		7	_aUY _2bicssc
072		7	_aCOM000000 _2bisacsh
072		7	_aUY _2thema
082	0	4	_a005.101/5113 _223/eng/20240528
049			_aMAIN
245	0	0	_aLogics and type systems in theory and practice : _bessays dedicated to Herman Geuvers on the occasion of his 60th birthday / _cVenanzio Capretta, Robbert Krebbers, Freek Wiedijk, editors.
264		1	_aCham : _bSpringer, _c[2024]
264		4	_c©2024
300			_a1 online resource (xii, 273 pages) : _billustrations (some color).
336			_atext _btxt _2rdacontent
337			_acomputer _bc _2rdamedia
338			_aonline resource _bcr _2rdacarrier
490	1		_aLecture notes in computer science, _x1611-3349 ; _v14560
500			_aIncludes author index.
520			_aThis Festschrift, dedicated to Herman Geuvers on the occasion of his 60th birthday, contains papers written by many of his closest collaborators. Herman Geuvers is a full professor at Radboud University Nijmegen and holds a part-time professorship at Eindhoven University of Technology. He received his PhD from Radboud University in 1993 and he was promoted to full professor in Computer Assisted Reasoning in 2006. Prof. Geuvers is an internationally renowned researcher in the field of proof assistants, logic in computer science, lambda calculus, and type theory. He has been a steering committee chair of the TYPES and FSCD conferences, chair of related EU Cost Action projects, and program chair or editor of related conferences and special issues in the area of computer science logic. He is a successful, generous and inspiring advisor and educator. He has been director of education and director of research of the Computer Science Institute at Radboud University Nijmegen, and he is currently chair of the examination board of computer science and chair of the board of the Institute for Programming Research and Algorithmics, a Dutch national inter-university research school. The contributions in this volume reflect Prof. Geuvers' main research interests.
588	0		_aOnline resource; title from PDF title page (SpringerLink, viewed May 28, 2024).
505	0		_aIntro -- 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
505	8		_a2 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
505	8		_a4.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
505	8		_a6 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
505	8		_a4.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
650		0	_aComputer logic. _96177
650		0	_aLambda calculus. _921584
650		0	_aType theory. _925498
650		6	_aLogique informatique. _919533
650		6	_aLambda-calcul. _927969
650		6	_aThéorie des types. _9976234
655		7	_aFestschriften. _2lcgft _9109631
700	1		_aCapretta, Venanzio, _eeditor. _9976235
700	1		_aKrebbers, Robbert, _eeditor. _9976236
700	1		_aWiedijk, Freek, _d1961- _eeditor. _1https://id.oclc.org/worldcat/entity/E39PBJf4gH7FR3TVpvdmCwfH4q _918769
700	1		_aGeuvers, Herman, _d1964- _ehonoree. _1https://id.oclc.org/worldcat/entity/E39PBJxxgPgWxkxJ3jydwK8XBP _918768
776	0	8	_iPrint version: _aCapretta, Venanzio _tLogics and Type Systems in Theory and Practice _dCham : Springer,c2024 _z9783031617157
830		0	_aLecture notes in computer science ; _v14560. _x1611-3349
856	4	0	_uhttps://link.springer.com/10.1007/978-3-031-61716-4
938			_aProQuest Ebook Central _bEBLB _nEBL31352123
994			_a92 _bATIST
999			_c656683 _d656683