awesome-philosophy-compsci icon indicating copy to clipboard operation
awesome-philosophy-compsci copied to clipboard

Published 20 hours ago • verified publisher icon glennstreet
→

Metadata

A list of resources that cross the disciplines of Computer Science and Philosophy

A curated list of awesome resources that bridge Philosophy and Computer Science. Last update: 2022-03-06

Related Sites

PhiloComp

"The aim of this website is to highlight the many strong links between Philosophy and Computing, for the benefit of students (and potential students) of both disciplines:…"

Encyclopedia Entries

Stanford Encyclopedia of Philosophy

Category Theory

Computability and Complexity

Computation in Physical Systems

Computational Complexity Theory

Computer and Information Ethics

Computing and Moral Responsibility

Information

The Lambda Calculus

Logic and Artificial Intelligence

Philosophy of Computer Science

Philosophy of Mathematics

Philosophy of Technology

Recursive Functions

Semantic Conceptions of Information

Set Theory

Internet Encyclopedia of Philosophy

Artificial Intelligence

The Brain in a Vat Argument

The Computational Theory of Mind

Wikipedia

Constraint logic programming

Logic Programming

Negation as failure

Bibliographies

Philosophy of Computing and Information at PhilPapers

Philosophy of Computer Science at DBLP

Books

Freely available

Philosophy of Computer Science by William Rapaport

Think Complexity, Second Edition by Allen Downey

Ontology of Philosophy of Computer Science

Internet Philosophy Ontology Project

Blogs

Bartosz Milewski's Programming Cafe

“Category Theory, Haskell, Concurrency, C++”

Gödel's Lost Letter and P=NP

Hillel Wayne's blog

Formal methods, including TLA+ and Alloy.

The n-Category Café

"A group blog on math, physics and philosophy". There is an associated wiki. “The nLab is a collaborative wiki. It grew out of the desire (I, II) to have a place for development (the ’Lab’ in ’nLab’) and indexed archives of the ideas and concepts surrounding the discussions at the The n-Category Café. These discussions primarily are about mathematics, physics and philosophy from the perspective of category theory and higher category theory (the ’n’ in ’nLab’ and nPOV).“

Shtetl-Optimized

Theory of Computing Blog Aggregator

Organizations and Societies

Association for Logic Programming

International Association for Computing And Philosophy

Conferences and Symposia

ACM/IEEE Symposium on Logic in Computer Science

Logic

An Automated Modal Reasoner

"This program takes lists of formalized sentences and checks them for consistency or validity in Propositional Modal Logic (S5 Axiom System)." Created by Brian Tackett.

Arend Theorem Prover

‘Arend implements a version of homotopy type theory with an interval type, which syntax is similar to cubical type theory. This implies several nice properties of path types and allows for a simple and clean definition of higher inductive types (including recursive ones).’

Argdown

A variation of markdown that allows one to create argument maps.

Carnap

"Carnap is a free and open software framework written in Haskell for teaching and studying formal logic." An introductory blog post by the author, Graham Leach-Krouse at Daily Nous.

Conan- A proof editor for first order logic

Coq Proof Assistant

Written in OCaml, "Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching."

GitHub repository

Home page of Wiki

GAPT: General Architecture for Proof Theory

‘GAPT is a proof theory framework developed primarily at the Vienna University of Technology. GAPT contains data structures, algorithms, parsers and other components common in proof theory and automated deduction. In contrast to automated and interactive theorem provers whose focus is the construction of proofs, GAPT concentrates on the transformation and further processing of proofs.’

List of Computational Tools for Modal Logic

Logic Matters

Microsoft's Lean

"Lean is an open source theorem prover and programming language being developed at Microsoft Research. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs."

Open Logic Project

Proof General

"Proof General is a generic interface for proof assistants (also known as interactive theorem provers), based on the extensible, customizable text editor Emacs." Since I'm an Emacs user, this has strong appeal.

SymPy Logic Module

"The logic module for SymPy allows to form and manipulate logic expressions using symbolic and Boolean values."

Taut

"This is a website that contains randomly-generated, self-correcting logic excercises. It runs directly on your browser, so there is no need to download anything. It was designed by Ariel Roffé (UBA / UNQ / CONICET), with support from the BA-Logic group"

Programming Languages and Libraries

Metamath

‘Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program.’

miniKanren

"miniKanren is an embedded Domain Specific Language for logic programming."

"miniKanren has been implemented in a growing number of host languages, including Scheme, Racket, Clojure, Haskell, Python, JavaScript, Scala, Ruby, OCaml, and PHP, among many other languages."

Lisp

Common Lisp

  1. The Common Lisp Cookbook

  2. Practical Common Lisp

    "If you think the greatest pleasure in programming comes from getting a lot done with code that simply and clearly expresses your intention, then programming in Common Lisp is likely to be about the most fun you can have with a computer. You'll get more done, faster, using it than you would using pretty much any other language."

Clojure

Scheme

Logica

‘We present Logica, a novel open source Logic Programming language. A successor to Yedalog (a language developed at Google earlier) it is a Datalog-like logic programming language. Logica code compiles to SQL and runs on Google BigQuery (with experimental support for PostgreSQL and SQLite), but it is much more concise and supports the clean and reusable abstraction mechanisms that SQL lacks. It supports modules and imports, it can be used from an interactive Python notebook and it even makes testing your queries natural and easy.’

Prolog

Awesome Prolog

A GitHub repository of Prolog awesomeness.

A. Aaby's Prolog Tutorial

J.R. Fisher's Prolog Tutorial

Metagol

‘Metagol is an inductive logic programming (ILP) system based on meta-interpretive learning. Metagol is written in Prolog and runs with SWI-Prolog.’

Paizo Prolog

'An ergonomic, mobile-first, Prolog playground!'

PrologHub

"PrologHub is dedicated to bringing together the Prolog community to share ideas and knowledge. Our aim is to encourage the growth and development of the community."

SWI-Prolog

Wikibooks Prolog

Picat

‘Picat is a simple, and yet powerful, logic-based multi-paradigm programming language aimed for general-purpose applications.’

Python

kanren

"Logic Programming in Python"

PySWIP

"PySWIP is a Python - SWI-Prolog bridge enabling to query SWI-Prolog in your Python programs. It features an (incomplete) SWI-Prolog foreign language interface, a utility class that makes it easy querying with Prolog and also a Pythonic interface."

truths - auto generate truth tables

tt - the Boolean expression toolbox

tt (truth table) is a library aiming to provide a Pythonic toolkit for working with Boolean expressions and truth tables.

Digital Philosophy

Articles tagged "digital humanities" at Daily Nous

Chris Alen Sula

"My work applies visualization and network science to humanities datasets, especially the history of philosophy. I also write on digital humanities and the politics of technology."

Philosopher's Web

A comprehensive map of all influential relationships in philosophy according to Wikipedia.

The Philosophome

Spinoza's Ethics 2.0

Created by Torin Doppelt

Digital Spinozism

Accompanying blog to Spinoza's Ethics 2.0

Transcribing Bentham

Why and How: Exploring the Significance of Digital Humanities for Philosophy

This is a presentation by Lisa Spirohttps://digitalscholarship.wordpress.com)

University Departments and Research Centers

Philosophy of Computer Science - Utrecht University

Magazines and Newsletters

ACM Transactions on Computational Logic (TOCL)

"For the purposes of ACM Transactions on Computational Logic, the field of computational logic consists of all uses of logic in computer science."

Newsletter on Philosophy and Computers - American Philosophical Association

Individual Philosophers

Colin Allen

Margaret A. Boden

Peter Bradley

David Chalmers

Jack Copeland

Staff page

Research profile

Daniel C. Dennett

Luciano Floridi

John MacFarlane

John is the creator of Pandoc.

Helen Nissenbaum

Gualtiero Piccinini

William J. Rapaport

Aaron Sloman

Edward N. Zalta

Philosophical Networks

Philosophical Wordnets

Contributed by Moses Boudorides, a series of Jupyter notebooks showing sentence-co-occurring relationships among concepts. Works analyzed include Heidegger's "The Question Concerning Technology" and Nietzsche's "Thus Spake Zarathustra".

Software for Philosophers

ArguMap

An iOS app for creating argument maps.

Hypernomicon

"Personal philosophy database software," created by Jason Winning.

← Metadata

67
Stars
4
Forks
Watchers

Owner

verified publisher icon glennstreet

Metadata

A list of resources that cross the disciplines of Computer Science and Philosophy

Back