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 491 articles , 4 standard articles )
Showing results 1 to 20 of 491.
Sorted by year (- 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)
- Schrijvers, Tom; Oliveira, Bruno C. D. S.; Wadler, Philip; Marntirosian, Koar: COCHIS: stable and coherent implicits (2019)
- Viroli, Mirko; Beal, Jacob; Damiani, Ferruccio; Audrito, Giorgio; Casadei, Roberto; Pianini, Danilo: From distributed coordination to field calculus and aggregate computing (2019)
- Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei: Verifying a scheduling protocol of safety-critical systems (2019)
- Blanqui, Frédéric: Size-based termination of higher-order rewriting (2018)
- Farka, František; Komendantskya, Ekaterina; Hammond, Kevin: Proof-relevant Horn clauses for dependent type inference and term synthesis (2018)
- Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
- Harper, Robert: Exception tracking in an open world (2018)
- Melham, Tom: Symbolic trajectory evaluation (2018)
- Paulson, Lawrence C.: Computational logic: its origins and applications (2018)
- Rossberg, Andreas: 1ML -- core and modules united (2018)
- Shankar, Natarajan: Combining model checking and deduction (2018)
- Shi, Ling; Zhao, Yongxin; Liu, Yang; Sun, Jun; Dong, Jin Song; Qin, Shengchao: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS (2018)
- Shi, Zhiping; Wu, Aixuan; Yang, Xiumei; Guan, Yong; Li, Yongdong; Song, Xiaoyu: Formal analysis of the kinematic Jacobian in screw theory (2018)
- Berger, Ulrich; Hou, Tie: A realizability interpretation of Church’s simple theory of types (2017)
- Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)