This volume contains research papers devoted to the theoretical foundations, design and application of computer systems for theory development. Such systems help to design mathematical axiomatization, perform computer-aided logical reasoning and manage databases of mathematical facts.

Proving strong normalization of CC by modifying realizability semantics.- Checking algorithms for Pure Type Systems.- Infinite objects in type theory.- Conservativity between logics and typed ? calculi.- Logic of refinement types.- Proof-checking a data link protocol.- Elimination of extensionality in Martin-Löf type theory.- Programming with streams in Coq a case study: The Sieve of Eratosthenes.- The Alf proof editor and its proof engine.- Encoding Z-style Schemas in type theory.- The expressive power of Structural Operational Semantics with explicit assumptions.- Developing certified programs in the system Coq the program tactic.- Closure under alpha-conversion.- Machine Deduction.- Type theory and the informal language of mathematics.- Semantics for abstract clauses.

GPSR Compliance The European Union's (EU) General Product Safety Regulation (GPSR) is a set of rules that requires consumer products to be safe and our obligations to ensure this. If you have any concerns about our products you can contact us on ProductSafety@springernature.com. In case Publisher is established outside the EU, the EU authorized representative is: Springer Nature Customer Service Center GmbH Europaplatz 3 69115 Heidelberg, Germany ProductSafety@springernature.com