Smart Contracts are executable specifications that can be uploaded to some distributed ledgers. Then their specification is executed and they become part of the chain when this is possible.
This allows the creation of certain kinds of business logic and data storage on top of a distributed ledger. How this works exactly is very dependent on the actual distributed ledger it is built on, of course.
This is a Community Wiki, so you can update the information in this post.
Ethereum allows you to create Turing Complete piece of code that are executed by the Ethereum Virtual Machine on the computers of the miners when they include transactions in the next block.
Because Smart Contracts are Turing Complete, a lot of creative ideas can be realized as Smart Contracts. On the other hand, this freedom makes it easy to introduce bugs.
Ethereum allows you to write Smart Contracts in four different languages that all compile to EVM bytecode, but currently only Solidity seems to be actively supported.
Unfortunately, development on Codius was halted in 2015.
Allows writing Smart Contracts that compile to EVM, and then use them on permissioned blockchains instead.
Corda is a distributed database that is not a Blockchain. Smart Contracts on Corda are written in any language that compiles to the Java Virtual Machine.
Plutus is a strictly typed pure functional programming language used for defining smart contracts in Cardano. The syntax is fairly Haskell-like, but unlike Haskell, the language is eagerly evaluated.