Related Research Articles
Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.
Peter John Landin was a British computer scientist. He was one of the first to realise that the lambda calculus could be used to model a programming language, an insight that is essential to the development of both functional programming and denotational semantics.
Nobuo Yoneda was a Japanese mathematician and computer scientist.
David A. Turner was a British computer scientist. He is best known for designing and implementing three programming languages, including the first for functional programming based on lazy evaluation, combinator graph reduction, and polymorphic types: SASL (1972), Kent Recursive Calculator (KRC) (1981), and the commercially supported Miranda (1985).
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human–machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.
Epigram is a functional programming language with dependent types, and the integrated development environment (IDE) usually packaged with the language. Epigram's type system is strong enough to express program specifications. The goal is to support a smooth transition from ordinary programming to integrated programs and proofs whose correctness can be checked and certified by the compiler. Epigram exploits the Curry–Howard correspondence, also termed the propositions as types principle, and is based on intuitionistic type theory.
In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like Agda, ATS, Coq, F*, Epigram, Idris, and Lean, dependent types help reduce bugs by enabling the programmer to assign types that further restrain the set of possible implementations.
Friedrich Ludwig "Fritz" Bauer was a German pioneer of computer science and professor at the Technical University of Munich.
Eric "Rick" C. R. Hehner is a Canadian computer scientist. He was born in Ottawa. He studied mathematics and physics at Carleton University, graduating with a Bachelor of Science (B.Sc.) in 1969. He studied computer science at the University of Toronto, graduating with a Master of Science (M.Sc.) in 1970, and a Doctor of Philosophy (Ph.D.) in 1974. He then joined the faculty there, becoming a full professor in 1983. He became the Bell University Chair in software engineering in 2001, and retired in 2012.
John Edward Lancelot Peck was the first permanent Head of Department of Computer Science at the University of British Columbia (UBC). He remained the Head of Department from 1969 to 1977.
The International Conference on Functional Programming (ICFP) is an annual academic conference in the field of computer science sponsored by the ACM SIGPLAN, in association with IFIP Working Group 2.8. The conference focuses on functional programming and related areas of programming languages, logic, compilers and software development.
Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version, originally named Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition.
Lambert Guillaume Louis Théodore Meertens or L.G.L.T. Meertens is a Dutch computer scientist and professor. As of 2020, he is a researcher at the Kestrel Institute, a nonprofit computer science research center in Palo Alto's Stanford Research Park.
Klaus Samelson was a German mathematician, physicist, and computer pioneer in the area of programming language translation and push-pop stack algorithms for sequential formula translation on computers.
In type theory, a discipline within mathematical logic, containers are abstractions which permit various "collection types", such as lists and trees, to be represented in a uniform way. A (unary) container is defined by a type of shapes S and a type family of positions P, indexed by S. The extension of a container is a family of dependent pairs consisting of a shape and a function from positions of that shape to the element type. Containers can be seen as canonical forms for collection types.
Roland Carl Backhouse is a British computer scientist and mathematician. As of 2020, he is Emeritus Professor of Computing Science at the University of Nottingham.
Jeremy Gibbons is a computer scientist and professor of computing at the University of Oxford. He serves as Deputy Director of the Software Engineering Programme in the Department of Computer Science, Governing Body Fellow at Kellogg College and Pro-Proctor of the University of Oxford.
ALF is a structure editor for monomorphic Martin-Löf type theory developed at Chalmers University. It is a predecessor of the Alfa, Agda, Cayenne and Coq proof assistants and dependently typed programming languages. It was the first language to support inductive families and dependent pattern matching.
Univalent foundations are an approach to the foundations of mathematics in which mathematical structures are built out of objects called types. Types in univalent foundations do not correspond exactly to anything in set-theoretic foundations, but they may be thought of as spaces, with equal types corresponding to homotopy equivalent spaces and with equal elements of a type corresponding to points of a space connected by a path. Univalent foundations are inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by "categorical" mathematics in the style of Alexander Grothendieck. Univalent foundations depart from the use of classical predicate logic as the underlying formal deduction system, replacing it, at the moment, with a version of Martin-Löf type theory. The development of univalent foundations is closely related to the development of homotopy type theory.
Thorsten Altenkirch is a German Professor of Computer Science at the University of Nottingham known for his research on logic, type theory, and homotopy type theory. Altenkirch was part of the 2012/2013 special year on univalent foundations at the Institute for Advanced Study. At Nottingham he co-chairs the Functional Programming Laboratory with Graham Hutton.
References
- ↑ "Dr Conor McBride: Reader: Computer and Information Sciences". University of Strathclyde: Computer and Information Sciences.
- ↑ McBride, Conor (July 2000). "Dependently Typed Functional Programs and their Proofs". Edinburgh Research Archive. University of Edinburgh. hdl:1842/374 . Retrieved 15 January 2016.
- ↑ McBride, Conor (1999). "Dependently Typed Functional Programs and their Proofs" (PDF). University of Edinburgh.
- ↑ Jeuring, Johan; Meertens, Lambert; Guttmann, Walter (17 August 2016). "Profile of IFIP Working Group 2.1". Foswiki. Retrieved 16 October 2020.
- ↑ Swierstra, Doaitse; Gibbons, Jeremy; Meertens, Lambert (2 March 2011). "ScopeEtc: IFIP21: Foswiki". Foswiki. Retrieved 16 October 2020.
- ↑ McBride, Conor. "Conor's Staring out the Window". Computer & Information Sciences. University of Strathclyde. Retrieved 18 August 2020.
- ↑ Altenkirch, Thorsten; McBride, Conor. "Towards Observational Type Theory" (PDF). StrictlyPositive.org.
- ↑ McBride, Conor; McKinna, James (January 2004). "The view from the left". Journal of Functional Programming. 14 (1): 69–111. doi: 10.1017/s0956796803004829 . S2CID 6232997.
- ↑ Cambridge Journals Online: Journal of Functional Programming, Conor McBride
