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 449 articles , 4 standard articles )
Showing results 1 to 20 of 449.
Sorted by year (- Farmer, William M.: Incorporating quotation and evaluation into Church’s type 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)
- Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Soundness and completeness proofs by coinductive methods (2017)
- Chihani, Zakaria; Miller, Dale; Renaud, Fabien: A semantic framework for proof evidence (2017)
- Crary, Karl: Modules, abstraction, and parametric polymorphism (2017)
- Farmer, William M.: Theory morphisms in Church’s type theory with quotation and evaluation (2017)
- Frohn, Florian; Giesl, Jürgen; Hensel, Jera; Aschermann, Cornelius; Ströder, Thomas: Lower bounds for runtime complexity of term rewriting (2017)
- Hou (Favonia), Kuen-Bang; Benton, Nick; Harper, Robert: Correctness of compiling polymorphism to dynamic typing (2017)
- Jha, Susmit; Seshia, Sanjit A.: A theory of formal synthesis via inductive learning (2017)
- Kammar, Ohad; Pretnar, Matija: No value restriction is needed for algebraic effects and handlers (2017)
- Kunčar, Ondřej; Popescu, Andrei: Comprehending Isabelle/HOL’s consistency (2017)
- Miller, Dale: Proof checking and logic programming (2017)
- Severi, Paula; Padovani, Luca; Tuosto, Emilio; Dezani-Ciancaglini, Mariangiola: On sessions and infinite data (2017)
- Zeyda, Frank; Foster, Simon; Freitas, Leo: An axiomatic value model for Isabelle/UTP (2017)
- Adams, Mark: HOL zero’s solutions for Pollack-inconsistency (2016)
- Ahmed, Waqar; Hasan, Osman; Tahar, Sofiène: Formalization of reliability block diagrams in higher-order logic (2016)
- Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
- Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
- Çiçek, Ezgi; Paraskevopoulou, Zoe; Garg, Deepak: A type theory for incremental computational complexity with control flow changes (2016)