ML
ML (’Meta Language’) is a general-purpose functional programming language. It has roots in Lisp, and has been characterized as ”Lisp with types”. It is known for its use of the polymorphic Hindley–Milner type system, which automatically assigns the types of most expressions without requiring explicit type annotations, and ensures type safety – there is a formal proof that a well-typed ML program does not cause runtime type errors.[1] ML provides pattern matching for function arguments, garbage collection, imperative programming, call-by-value and currying. It is used heavily in programming language research and is one of the few languages to be completely specified and verified using formal semantics. Its types and pattern matching make it well-suited and commonly used to operate on other formal languages, such as in compiler writing, automated theorem proving and formal verification. (wikipedia)
Keywords for this software
References in zbMATH (referenced in 517 articles , 4 standard articles )
Showing results 1 to 20 of 517.
Sorted by year (- Christensen, Michael; McMahan, Joseph; Nichols, Lawton; Roesch, Jared; Sherwood, Timothy; Hardekopf, Ben: Safe functional systems through integrity types and verified assembly (2021)
- Ahmad, Waqar; Hasan, Osman; Tahar, Sofiène: Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation (2020)
- Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
- Barendregt, Henk P.: Gems of Corrado Böhm (2020)
- Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
- Bry, François: In praise of impredicativity: a contribution to the formalization of meta-programming (2020)
- Karachalias, Georgios; Pretnar, Matija; Saleh, Amr Hany; Vanderhallen, Stien; Schrijvers, Tom: Explicit effect subtyping (2020)
- Kaufmann, Matt; Moore, J Strother: Limited second-order functionality in a first-order setting (2020)
- Rashid, Adnan; Hasan, Osman: Formal verification of robotic cell injection systems up to 4-DOF using \textsfHOLLight (2020)
- Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2020)
- Tian, Chun; Sangiorgi, Davide: Unique solutions of contractions, CCS, and their HOL formalisation (2020)
- Zhang, Xingyuan; Urban, Christian; Wu, Chunhan: Priority inheritance protocol proved correct (2020)
- García-Pérez, Álvaro; Nogueira, Pablo: The full-reducing krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus (2019)
- Jay, Barry: Intensional computation with higher-order functions (2019)
- Kunčar, Ondřej; Popescu, Andrei: A consistent foundation for Isabelle/HOL (2019)
- Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
- Li, Li-Ming; Shi, Zhi-Ping; Guan, Yong; Zhang, Qian-Ying; Li, Yong-Dong: Formalization of geometric algebra in HOL Light (2019)
- Miller, Dale: Mechanized metatheory revisited (2019)
- Moore, J. Strother: Milestones from the Pure Lisp Theorem Prover to ACL2 (2019)
- Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)