The following pages link to ML (Q13958):
Displaying 50 items.
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- A revision of the proof of the Kepler conjecture (Q977177) (← links)
- Typing termination in a higher-order concurrent imperative language (Q979082) (← links)
- An overview of the K semantic framework (Q987974) (← links)
- Type inference and strong static type checking for Promela (Q988201) (← links)
- Formalization of the standard uniform random variable (Q995466) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- A rewriting logic approach to operational semantics (Q1012130) (← links)
- Recasting ML\(^{\text F}\) (Q1023287) (← links)
- Adapting functional programs to higher order logic (Q1029815) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- Data compression for proof replay (Q1040776) (← links)
- Using theorem proving to verify expectation and variance for discrete random variables (Q1040780) (← links)
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050) (← links)
- On the existence of free models in abstract algebraic institutions (Q1085969) (← links)
- A characterization of F-complete type assignments (Q1089331) (← links)
- Toward formal development of programs from algebraic specifications: Implementations revisited (Q1090100) (← links)
- Quasi-varieties in abstract algebraic institutions (Q1091132) (← links)
- An algebraic semantics approach to the effective resolution of type equations (Q1093359) (← links)
- Pebble, a kernel language for modules and abstract data types (Q1104071) (← links)
- A semantics of multiple inheritance (Q1106652) (← links)
- Principal type scheme and unification for intersection type discipline (Q1110311) (← links)
- Polymorphic type inference and containment (Q1110312) (← links)
- On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory (Q1120558) (← links)
- Generalization from partial parametrization in higher-order type theory (Q1122980) (← links)
- Higher-order rewrite systems and their confluence (Q1127334) (← links)
- Efficient high-level parallel programming (Q1128713) (← links)
- Polymorphic syntax definition (Q1129122) (← links)
- Algebraic processing of programming languages (Q1129126) (← links)
- An efficient interpreter for the lambda-calculus (Q1158139) (← links)
- A rewrite-based type discipline for a subset of computer algebra (Q1176783) (← links)
- Co-induction in relational semantics (Q1177158) (← links)
- Type checking with universes (Q1177937) (← links)
- Static semantics, types, and binding time analysis (Q1179698) (← links)
- Modularising the specification of a small database system in extended ML (Q1184686) (← links)
- On the expressive power of finitely typed and universally polymorphic recursive procedures (Q1185006) (← links)
- \(\pi\)-RED - a graph reducer for a full-fledged \(\lambda\)-calculus (Q1186104) (← links)
- A typed functional extension of logic programming (Q1186105) (← links)
- Optimal parallel algorithms for forest and term matching (Q1186605) (← links)
- Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus (Q1193590) (← links)
- Complete restrictions of the intersection type discipline (Q1193654) (← links)
- On subsumption and semiunification in feature algebras (Q1194340) (← links)
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations (Q1196302) (← links)
- The revised report on the syntactic theories of sequential control and state (Q1199538) (← links)
- Constructing type systems over an operational semantics (Q1199709) (← links)
- Safety analysis versus type inference for partial types (Q1199876) (← links)
- On the synthesis of function inverses (Q1205183) (← links)
- Principal types of BCK-lambda-terms (Q1208417) (← links)
- Theories for mechanical proofs of imperative programs (Q1267030) (← links)
- Extending the type checker of Standard ML by polymorphic recursion (Q1275627) (← links)
