The following pages link to ML (Q13958):
Displaying 50 items.
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
- Implementing geometric algebra products with binary trees (Q742367) (← links)
- The semantics of second-order lambda calculus (Q751294) (← links)
- Type inference with recursive types: Syntax and semantics (Q756435) (← links)
- Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions (Q764331) (← links)
- Bio-PEPAd: a non-Markovian extension of Bio-PEPA (Q764354) (← links)
- Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation (Q782499) (← links)
- Completeness of type assignment in continuous lambda models (Q792995) (← links)
- A polymorphic type system for Prolog (Q796313) (← links)
- Type inference for record concatenation and multiple inheritance (Q808687) (← links)
- Logic-based subsumption architecture (Q814558) (← links)
- A complete mechanization of correctness of a string-preprocessing algorithm (Q816208) (← links)
- Two case studies of semantics execution in Maude: CCS and LOTOS (Q816216) (← links)
- Formalization of fixed-point arithmetic in HOL (Q816219) (← links)
- High-level modelling for typed functional programming (Q832100) (← links)
- Efficient virtual machine support of runtime structural reflection (Q838165) (← links)
- Proof pearl: Mechanizing the textbook proof of Huffman's algorithm (Q839031) (← links)
- Compilation of extended recursion in call-by-value functional languages (Q848739) (← links)
- Simplifying proofs in Fitch-style natural deduction systems (Q851139) (← links)
- Ordinal arithmetic: Algorithms and mechanization (Q851144) (← links)
- Polymorphic typed defunctionalization and concretization (Q853737) (← links)
- Formal compiler construction in a logical framework (Q853741) (← links)
- Type checking a multithreaded functional language with session types (Q859841) (← links)
- Bisimilarity is not finitely based over BPA with interrupt (Q860878) (← links)
- Deciding Boolean algebra with Presburger arithmetic (Q861705) (← links)
- TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
- A proof-centric approach to mathematical assistants (Q865648) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Database query languages and functional logic programming (Q867491) (← links)
- Verification of FPGA layout generators in higher-order logic (Q877830) (← links)
- Providing a formal linkage between MDG and HOL (Q878110) (← links)
- The Girard-Reynolds isomorphism (second edition) (Q879366) (← links)
- A few exercises in theorem processing (Q879370) (← links)
- A new generic scheme for functional logic programming with constraints (Q880985) (← links)
- A complete axiom system for propositional projection temporal logic with cylinder computation model (Q896162) (← links)
- Formal probabilistic analysis of detection properties in wireless sensor networks (Q903510) (← links)
- Meta-circular interpreter for a strongly typed language (Q908683) (← links)
- Constructive system for automatic program synthesis (Q912589) (← links)
- Deforestation: Transforming programs to eliminate trees (Q914358) (← links)
- Semantics of types for database objects (Q915443) (← links)
- Type inference for polymorphic references (Q918190) (← links)
- The calculus of context relations (Q918720) (← links)
- A mechanical analysis of program verification strategies (Q928673) (← links)
- Extending FeatherTrait Java with interfaces (Q930885) (← links)
- Towards proving type safety of .NET CIL (Q941469) (← links)
- Proof synthesis and reflection for linear arithmetic (Q945055) (← links)
- The seven virtues of simple type theory (Q946569) (← links)
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms (Q964000) (← links)
- Programming with narrowing: a tutorial (Q968524) (← links)
