Idris is a programming language which encourages “type-driven development”. We believe that to enable the highest levels of productivity, programming should be a conversation between the programmer and the machine. A…
Linear logic is a refinement of traditional (or classical) logic which is conscious of resource usage, and tracks resources carefully. This logic has many applications in Computer Science (such as in the design of…
Dependently-typed programming languages, such as Idris and Agda, permit the use of logical properties to constrain the values an expression could take. This allows us to incorporate the proof that a program satisfies…
Functional programming is a programming paradigm which comprises equations between functions operating on “abstract data”. It is a very neat and concise style that focuses on the core logic rather than catering to the…
Keywords Compilers, Programming Languages, Code Generation, Systems Programming Staff [Christopher Brown]{cmb21}
Keywords Programming languages, Types Staff [Edwin Brady]{ecb10}