scientific article; zbMATH DE number 234014
From MaRDI portal
Publication:5287513
Recommendations
Cited in
(only showing first 100 items - show all)- Unifying Sets and Programs via Dependent Types
- Comprehending Isabelle/HOL’s Consistency
- An untyped higher order logic with Y combinator
- Proof search with set variable instantiation in the calculus of constructions
- Structuring metatheory on inductive definitions
- Characteristics of de Bruijn’s early proof checker Automath
- From types to sets by local type definition in higher-order logic
- An approach to formal verification of human-computer interaction
- Unique solutions of contractions, CCS, and their HOL formalisation
- A realizability interpretation of Church's simple theory of types
- On the desirability of mechanizing calculational proofs
- Scalable fine-grained proofs for formula processing
- Solving modal logic problems by translation to higher-order logic
- A scalable module system
- From types to sets by local type definitions in higher-order logic
- Proof assistance for real-time systems using an interactive theorem prover
- Formal Analysis of Optical Waveguides in HOL
- Extended Static Checking by Calculation Using the Pointfree Transform
- Two case studies of semantics execution in Maude: CCS and LOTOS
- Unifying sets and programs via dependent types
- Semantic essence of AsmL
- A comparison of HOL and ALF formalizations of a categorical coherence theorem
- A proof tool for reasoning about functional programs
- A Mizar mode for HOL
- A comparison of MDG and HOL for hardware verification
- A structure preserving encoding of Z in Isabelle/HOL
- A mechanisation of computability theory in HOL
- Elements of mathematical analysis in PVS
- Formal verification of algorithm \(\mathcal{W}\): the monomorphic case
- Importing mathematics from HOL into Nuprl
- Set theory, higher order logic or both?
- Translating specifications in VDM-SL to PVS
- Towards applying the composition principle to verify a microkernel operating system
- Winskel is (almost) right. Towards a mechanized semantics textbook
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
- Proof pearl: Mechanizing the textbook proof of Huffman's algorithm
- Adapting functional programs to higher order logic
- Formal reliability analysis of combinational circuits using theorem proving
- Reasoning about conditional probabilities in a higher-order-logic theorem prover
- Twenty Years of Theorem Proving for HOLs Past, Present and Future
- Theories for mechanical proofs of imperative programs
- Abstracting communication to reason about distributed algorithms
- The seven virtues of simple type theory
- Using Structural Recursion for Corecursion
- Formal verification of a programming logic for a distributed programming language
- Formal analysis of the kinematic Jacobian in screw theory
- Extensional higher-order paramodulation in Leo-III
- The Imandra Automated Reasoning System (System Description)
- The proof monad
- scientific article; zbMATH DE number 2185697 (Why is no real title available?)
- Automated reasoning for probabilistic sequential programs with theorem proving
- The HOL-Omega Logic
- A decision procedure for linear ``big O equations
- Mechanized metatheory revisited
- Dealing with algebraic expressions over a field in Coq using Maple
- Efficient substitution in Hoare logic expressions
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- Simplifying proofs in Fitch-style natural deduction systems
- LCF-style Platform based on Multiway Decision Graphs
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
- Programmed strategies for program verification
- Interpreting HOL in the calculus of constructions
- The higher-order prover \textsc{Leo}-II
- Semi-intelligible Isar proofs from machine-generated proofs
- scientific article; zbMATH DE number 1424012 (Why is no real title available?)
- A theory of formal synthesis via inductive learning
- scientific article; zbMATH DE number 2090293 (Why is no real title available?)
- Program derivation with verified transformations — a case study
- Higher-order rewrite systems and their confluence
- Combining higher-order logic with set theory formalizations
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Combining Decision Procedures by (Model-)Equality Propagation
- A Brief Overview of HOL4
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
- Formalizing an analytic proof of the prime number theorem
- A framework for the verification of certifying computations
- Incorporating quotation and evaluation into Church's type theory
- Combining decision procedures by (model-)equality propagation
- Mechanised wire-wise verification of Handel-C synthesis
- Monotonicity inference for higher-order formulas
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
- Auto in Agda. Programming proof search using reflection
- Higher-order semantics and extensionality
- The strategy challenge in SMT solving
- A proof-centric approach to mathematical assistants
- A formal proof of the Kepler conjecture
- Assumption-based runtime verification
- Incorporating quotation and evaluation into Church's type theory: syntax and semantics
- Formalization of the standard uniform random variable
- Analytic tableaux for higher-order logic with choice
- Monotonicity inference for higher-order formulas
- Local Theory Specifications in Isabelle/Isar
- Isabelle/HOL. A proof assistant for higher-order logic
- Superposition with lambdas
- Abstraction of hardware construction
- R n - and G n -logics
- Reflection of formal tactics in a deductive reflection framework
- Circuits as streams in Coq: verification of a sequential multiplier
- Computer supported mathematics with MEGA
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 Q5287513)
