[{"id":16,"name":"Agda","slug":"agda","description":"Agda is a dependently typed programming language that supports formal verification. It is primarily used for writing correct and trustworthy software, as well as for mathematical proofs and research in type theory.","execution_mechanism":"compiled","logo_svg":null,"repo_url":null,"website_url":"https:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php","wikipedia_url":"https:\/\/en.wikipedia.org\/wiki\/Agda_(programming_language)","appeared_on":null,"latest_release_date":null,"latest_release_version":null,"created_on":"2023-08-22 15:02:36","github_repo_count":2472,"paradigms":"28","typings":"7,8,9,57,61,62","oses":"2,3"},{"id":45,"name":"ATS","slug":"ats","description":"ATS is a statically-typed programming language that supports both functional and imperative programming paradigms. It is primarily used for systems-level programming, concurrent and parallel programming, and formal verification of software systems.","execution_mechanism":"compiled","logo_svg":null,"repo_url":null,"website_url":"http:\/\/www.ats-lang.org\/","wikipedia_url":"https:\/\/en.wikipedia.org\/wiki\/ATS_(programming_language)","appeared_on":null,"latest_release_date":null,"latest_release_version":null,"created_on":"2023-08-22 15:02:40","github_repo_count":223,"paradigms":"6,10","typings":"8,62,95","oses":null},{"id":81,"name":"Cayenne","slug":"cayenne","description":"The 'Cayenne' programming language is a statically-typed, general-purpose language with a focus on simplicity and readability. It is used for a wide range of applications including web development, data analysis, and system programming.","execution_mechanism":"interpreted","logo_svg":null,"repo_url":null,"website_url":null,"wikipedia_url":"https:\/\/en.wikipedia.org\/wiki\/Cayenne_(programming_language)","appeared_on":null,"latest_release_date":null,"latest_release_version":null,"created_on":"2023-08-22 15:02:45","github_repo_count":null,"paradigms":"10","typings":"62","oses":null},{"id":158,"name":"Epigram","slug":"epigram","description":"Epigram is a dependently typed functional programming language with a focus on formal verification. It is primarily used for writing certified software, proving the correctness of programs, and developing formal proofs.","execution_mechanism":"other","logo_svg":null,"repo_url":null,"website_url":"http:\/\/e-pig.org","wikipedia_url":"https:\/\/en.wikipedia.org\/wiki\/Epigram_(programming_language)","appeared_on":null,"latest_release_date":null,"latest_release_version":null,"created_on":"2023-08-22 15:02:57","github_repo_count":null,"paradigms":"10","typings":"8,9,62","oses":null},{"id":170,"name":"F*","slug":"fstar","description":"The F* programming language is a dependently typed functional programming language that is designed to verify the correctness of programs. Its main uses include programming language research, program synthesis, and formal verification of software and security protocols.","execution_mechanism":"other","logo_svg":null,"repo_url":null,"website_url":"https:\/\/www.fstar-lang.org\/","wikipedia_url":"https:\/\/en.wikipedia.org\/wiki\/F*_(programming_language)","appeared_on":null,"latest_release_date":null,"latest_release_version":null,"created_on":"2023-08-22 15:02:59","github_repo_count":314,"paradigms":"8,10","typings":"7,8,9,62,113","oses":"7"},{"id":244,"name":"Idris","slug":"idris","description":"Idris is a general-purpose, purely functional programming language with dependent types. It is primarily used for research in formal methods, theorem proving, and programming language design.","execution_mechanism":"compiled","logo_svg":null,"repo_url":null,"website_url":"https:\/\/www.idris-lang.org","wikipedia_url":"https:\/\/en.wikipedia.org\/wiki\/Idris_(programming_language)","appeared_on":null,"latest_release_date":null,"latest_release_version":null,"created_on":"2023-08-22 15:03:09","github_repo_count":2049,"paradigms":"10,28,93","typings":"8,62,95,214","oses":null}]