The following pages link to ML (Q13958):
Displaying 50 items.
- Contract-based verification of MATLAB-style matrix programs (Q282101) (← links)
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (Q287361) (← links)
- Formalization of reliability block diagrams in higher-order logic (Q334147) (← links)
- Effect-polymorphic behaviour inference for deadlock checking (Q338624) (← links)
- Functorial semantics of first-order views (Q344796) (← links)
- A two-valued logic for properties of strict functional programs allowing partial functions (Q352946) (← links)
- An approach for lifetime reliability analysis using theorem proving (Q386029) (← links)
- Semantic types and approximation for Featherweight Java (Q387991) (← links)
- An observationally complete program logic for imperative higher-order functions (Q387994) (← links)
- Full abstraction for Reduced ML (Q388212) (← links)
- Unifying sets and programs via dependent types (Q408534) (← links)
- Mechanised support for sound refinement tactics (Q432151) (← links)
- Monotonicity inference for higher-order formulas (Q438558) (← links)
- Analytic tableaux for higher-order logic with choice (Q438561) (← links)
- Exploring structural symmetry automatically in symbolic trajectory evaluation (Q453494) (← links)
- Core FOBS: A hybrid functional and object-oriented language (Q456463) (← links)
- Automatic verification of reduction techniques in higher order logic (Q469363) (← links)
- An inductive approach to strand spaces (Q470008) (← links)
- Formal analysis of optical systems (Q475384) (← links)
- Programming with algebraic effects and handlers (Q478396) (← links)
- The complexity of higher-order queries (Q498405) (← links)
- An approach to completing variable names for implicitly typed functional languages (Q526448) (← links)
- On graph rewriting, reduction, and evaluation in the presence of cycles (Q526460) (← links)
- A language for generic programming in the large (Q532409) (← links)
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4 (Q540690) (← links)
- A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL (Q541222) (← links)
- Reasoning about conditional probabilities in a higher-order-logic theorem prover (Q545151) (← links)
- Formal reliability analysis of combinational circuits using theorem proving (Q545153) (← links)
- The correctness of Newman's typability algorithm and some of its extensions (Q549191) (← links)
- Computability in higher types, P\(\omega\) and the completeness of type assignment (Q579245) (← links)
- Generating meta-heuristic optimization code using ADATE (Q604934) (← links)
- Specifying rewrite strategies for interactive exercises (Q626940) (← links)
- Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\) (Q636376) (← links)
- Linearity and iterator types for Gödel's system \(\mathcal T\) (Q656851) (← links)
- Forum: A multiple-conclusion specification logic (Q671512) (← links)
- From CML to its process algebra (Q672132) (← links)
- Term rewriting and Hoare logic -- Coded rewriting (Q673226) (← links)
- Precedences in specifications and implementations of programming languages (Q673491) (← links)
- On the role of memory in object-based and object-oriented languages (Q674010) (← links)
- Mapping a functional notation for parallel programs onto hypercubes (Q674270) (← links)
- Reusing and modifying rulebases by predicate substitution (Q676430) (← links)
- Region-based memory management (Q676777) (← links)
- Categorical ML -- category-theoretic modular programming (Q684395) (← links)
- Computational interpretations of linear logic (Q685430) (← links)
- Polymorphic type inference for the relational algebra (Q696968) (← links)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (Q703860) (← links)
- Exception tracking in an open world (Q724930) (← links)
- Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application (Q736916) (← links)
