scientific article; zbMATH DE number 958048
From MaRDI portal
Publication:5687569
Recommendations
- scientific article; zbMATH DE number 709076
- scientific article; zbMATH DE number 49256
- scientific article; zbMATH DE number 578226
- Concurrent Programming in ML
- Concurrent Programming in ML
- scientific article; zbMATH DE number 578225
- scientific article; zbMATH DE number 1027560
- scientific article; zbMATH DE number 1678394
Cited in
(53)- Using theorem proving to verify expectation and variance for discrete random variables
- A notation for lambda terms. A generalization of environments
- A co-induction principle for recursively defined domains
- Deductive and inductive synthesis of equational programs
- PCF extended with real numbers
- Essential concepts of algebraic specification and program development
- The definition of Extended ML: A gentle introduction
- Formal analysis of continuous-time systems using Fourier transform
- Modeling message queueing services with reliability guarantee in cloud computing environment using colored Petri nets
- Amalgamation in the semantics of CASL
- Organizing numerical theories using axiomatic type classes
- A tactic calculus. --- Abridged version
- Mechanising the theory of intervals using OBJ3
- Unifying theories in ProofPower-Z
- The locally nameless representation
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
- Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light}
- Priority inheritance protocol proved correct
- Proof pearl: A mechanized proof of GHC's mergesort
- On the formalization of gamma function in HOL
- Types for modules
- Decidability of bounded higher-order unification
- Shallow confluence of conditional term rewriting systems
- Compensation methods to support cooperative applications: A case study in automated verification of schema requirements for an advanced transaction model
- The Orc Programming Language
- Mechanised support for sound refinement tactics
- Exploring structural symmetry automatically in symbolic trajectory evaluation
- An inductive approach to strand spaces
- Demonstrating Lambda Calculus Reduction
- Pixel Geometry
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
- F-ing modules
- A fixedpoint approach to implementing (co)inductive definitions
- 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
- Evaluation of anonymity and confidentiality protocols using theorem proving
- Formalising Mathematics in Simple Type Theory
- Verifying feedforward neural networks for classification in Isabelle/HOL
- Specifying rewrite strategies for interactive exercises
- Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
- On the role of memory in object-based and object-oriented languages
- Should ML be object-oriented?
- Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
- The HOL-CSP Refinement Toolkit
- Priority Queues Based on Braun Trees
- Integration theory and random variables
- HOL-CSP Version 2.0
- A Sound Type System for Physical Quantities, Units, and Measurements
- Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation
- Providing a formal linkage between MDG and HOL
- A few exercises in theorem processing
- Formalization of the standard uniform random variable
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 Q5687569)
