Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

"Type theory is a fast-evolving field at the crossroads of logic, computer science and mathematics. This gentle step-by-step introduction is ideal for graduate students and researchers who need to understand the ins and outs of the mathematical machinery, the role of logical rules therein, the essential contribution of definitions and the decisive nature of well-structured proofs. The authors begin with untyped lambda calculus and proceed to several fundamental type systems culminating in the well-known and powerful Calculus of Constructions. The book also covers the essence of proof checking and proof development, and the use of dependent type theory to formalize mathematics. The only prerequisites are a good knowledge of undergraduate algebra and analysis. Carefully chosen examples illustrate the theory throughout. Each chapter ends with a summary of the content, some historical context, suggestions for further reading and a selection of exercises to help readers familiarize themselves with the material"--

Type theory. --- Computers --- Programming Languages --- General. --- Théorie des types

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

These proceedings contain a refereed selection of papers presented at the Second Annual Workshop of the Types Working Group (Computer-Assisted Reasoning based on Type Theory, EUIST project 29001), which was held April 24–28, 2002 in Hotel Erica, Berg en Dal (close to Nijmegen), The Netherlands. The workshop was attended by about 90 researchers. On April 27, there was a special afternoon celebrating the 60th birthday of Per Martin-L¨of, one of the founding fathers of the Types community. The afternoon consisted of the following three invited talks: “Constructive Validity Revisited” by Dana Scott, “From the Rules of Logic to the Logic of Rules” by Jean-Yves Girard, and “The Varieties of Type Theories” by Peter Aczel. The contents of these contributions were not laid down in these proceedings, but the videos of the talks and the slides used by the speakers are available at http://www. cs. kun. nl/fnds/MartinLoefDay/LoefTalks. htm The previous workshop of the Types Working Group under EUIST project 29001 was held in 2000 in Durham, UK. The workshops Types 2000 and Types 2002 followed a series of meetings organized in the period 1993 – 1999 whithin previous Types projects (ESPRIT BRA 6435 and ESPRIT Working Group 21900). The proceedings of these earlier Types workshops were also published in the LNCS series, as volumes 806, 996, 1158, 1512, 1657, 1956 and 2277. ESPRIT BRA 6453 was a continuation of ESPRIT Action 3245, Logical Frameworks: - sign, Implementation and Experiments.

Automatic theorem proving --- Computer programming --- Computer Science --- Engineering & Applied Sciences --- Computer science. --- Science. --- Software engineering. --- Programming languages (Electronic computers). --- Computers. --- Computer logic. --- Mathematical logic. --- Computer Science. --- Software Engineering/Programming and Operating Systems. --- Science, general. --- Theory of Computation. --- Logics and Meanings of Programs. --- Programming Languages, Compilers, Interpreters. --- Mathematical Logic and Formal Languages. --- Information theory. --- Logic design. --- Science, Humanities and Social Sciences, multidisciplinary. --- Informatics --- Science --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Machine theory --- Switching theory --- Communication theory --- Communication --- Cybernetics --- Computer software engineering --- Engineering --- Algebra of logic --- Logic, Universal --- Mathematical logic --- Symbolic and mathematical logic --- Symbolic logic --- Mathematics --- Algebra, Abstract --- Metamathematics --- Set theory --- Syllogism --- Computer languages --- Computer program languages --- Computer programming languages --- Machine language --- Electronic data processing --- Languages, Artificial --- Computer science logic --- Logic, Symbolic and mathematical --- Automatic computers --- Automatic data processors --- Computer hardware --- Computing machines (Computers) --- Electronic brains --- Electronic calculating-machines --- Electronic computers --- Hardware, Computer --- Computer systems --- Calculators --- Cyberspace --- Programming languages (Electronic computers) --- Logic, Symbolic and mathematical.

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

This book constitutes the refereed proceedings of the 10th International Conference on Intelligent Computer Mathematics, CICM 2017, held in Edinburgh, Scotland, in July 2017. The 22 full papers and 3 abstracts of invited papers presented were carefully reviewed and selected from a total of 40 submissions. The papers are organized in three tracks: the Calculemus track examining the integration of symbolic computation and mechanized reasoning; the Digital Mathematics Libraries track dealing with math-aware technologies, standards, algorithms, and processes; the Mathematical Knowledge Management track being concerned with all aspects of managing mathematical knowledge, in informal, semi-formal, and formal settings. An additional track Systems and Projects contains descriptions of systems and relevant projects, both of which are key to a research topic where theory and practice interact on explicitly represented knowledge.

Computer science. --- Software engineering. --- Programming languages (Electronic computers). --- Computer logic. --- Mathematical logic. --- Artificial intelligence. --- Computer simulation. --- Computer Science. --- Artificial Intelligence (incl. Robotics). --- Mathematical Logic and Formal Languages. --- Logics and Meanings of Programs. --- Software Engineering. --- Programming Languages, Compilers, Interpreters. --- Simulation and Modeling. --- Computer modeling --- Computer models --- Modeling, Computer --- Models, Computer --- Simulation, Computer --- AI (Artificial intelligence) --- Artificial thinking --- Electronic brains --- Intellectronics --- Intelligence, Artificial --- Intelligent machines --- Machine intelligence --- Thinking, Artificial --- Computer science logic --- Computer languages --- Computer program languages --- Computer programming languages --- Machine language --- Computer software engineering --- Informatics --- Algebra of logic --- Logic, Universal --- Mathematical logic --- Symbolic and mathematical logic --- Symbolic logic --- Electromechanical analogies --- Mathematical models --- Simulation methods --- Model-integrated computing --- Bionics --- Cognitive science --- Digital computer simulation --- Electronic data processing --- Logic machines --- Machine theory --- Self-organizing systems --- Fifth generation computers --- Neural computers --- Logic, Symbolic and mathematical --- Languages, Artificial --- Engineering --- Science --- Mathematics --- Algebra, Abstract --- Metamathematics --- Set theory --- Syllogism --- Logic design. --- Artificial Intelligence. --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Switching theory

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

This book constitutes the refereed proceedings of the Second International Conference on Interactive Theorem proving, ITP 2011, held in Berg en Dal, The Netherlands, in August 2011. The 25 revised full papers presented were carefully reviewed and selected from 50 submissions. Among the topics covered are counterexample generation, verification, validation, term rewriting, theorem proving, computability theory, translations from one formalism to another, and cooperation between tools. Several verification case studies were presented, with applications to computational geometry, unification, real analysis, etc.

Mathematical logic --- Logic --- Computer science --- Programming --- Artificial intelligence. Robotics. Simulation. Graphics --- Computer. Automation --- ontwerpen --- programmeren (informatica) --- programmeertalen --- wiskunde --- software engineering --- robots