scientific article; zbMATH DE number 958048
From MaRDI portal
Publication:5687569
zbMath0863.68032MaRDI QIDQ5687569
Publication date: 16 December 1996
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Theory of programming languages (68N15) General topics in the theory of software (68N01)
Related Items
Types for modules ⋮ PCF extended with real numbers ⋮ Formal analysis of continuous-time systems using Fourier transform ⋮ Modeling message queueing services with reliability guarantee in cloud computing environment using colored Petri nets ⋮ Mechanising the theory of intervals using OBJ3 ⋮ Essential concepts of algebraic specification and program development ⋮ Providing a formal linkage between MDG and HOL ⋮ A few exercises in theorem processing ⋮ A notation for lambda terms. A generalization of environments ⋮ The definition of Extended ML: A gentle introduction ⋮ Formalising Mathematics in Simple Type Theory ⋮ Specifying rewrite strategies for interactive exercises ⋮ Unifying theories in ProofPower-Z ⋮ Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light} ⋮ Verifying feedforward neural networks for classification in Isabelle/HOL ⋮ The locally nameless representation ⋮ A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL ⋮ Mechanised support for sound refinement tactics ⋮ Exploring structural symmetry automatically in symbolic trajectory evaluation ⋮ An inductive approach to strand spaces ⋮ Decidability of bounded higher-order unification ⋮ On the role of memory in object-based and object-oriented languages ⋮ Compensation methods to support cooperative applications: A case study in automated verification of schema requirements for an advanced transaction model ⋮ Demonstrating Lambda Calculus Reduction ⋮ Pixel Geometry ⋮ A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL ⋮ Reasoning about conditional probabilities in a higher-order-logic theorem prover ⋮ Formal reliability analysis of combinational circuits using theorem proving ⋮ Amalgamation in the semantics of CASL ⋮ Organizing numerical theories using axiomatic type classes ⋮ Formalization of the standard uniform random variable ⋮ Evaluation of anonymity and confidentiality protocols using theorem proving ⋮ Shallow confluence of conditional term rewriting systems ⋮ A fixedpoint approach to implementing (Co)inductive definitions ⋮ Priority inheritance protocol proved correct ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ The Orc Programming Language ⋮ A tactic calculus. --- Abridged version ⋮ F-ing modules ⋮ Using theorem proving to verify expectation and variance for discrete random variables ⋮ Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation ⋮ A co-induction principle for recursively defined domains ⋮ Proof pearl: A mechanized proof of GHC's mergesort ⋮ On the formalization of gamma function in HOL ⋮ Deductive and inductive synthesis of equational programs
Uses Software
