scientific article; zbMATH DE number 2003161
From MaRDI portal
Publication:4435474
zbMATH Open1023.68657MaRDI QIDQ4435474FDOQ4435474
Authors: Tobias Nipkow 
Publication date: 12 November 2003
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2646/26460259.htm
Title of this publication is not available (Why is that?)
Cited In (14)
- Representing model theory in a type-theoretical logical framework
- Verified Real Asymptotics in Isabelle/HOL
- Formalizing axiomatic systems for propositional logic in Isabelle/HOL
- The Isabelle Framework
- The teaching tool CalcCheck: a proof-checker for Gries and Schneider's ``Logical approach to discrete math
- Types for Proofs and Programs
- Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle
- Mathematical method and proof
- Introduction to ``Milestones in interactive theorem proving
- Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
- Title not available (Why is that?)
- Proving pointer programs in higher-order logic
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools
- More Church-Rosser proofs (in Isabelle/HOL)
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4435474)
