A dedução natural e o cálculo de sequentes são dois dos principais sistemas de dedução formal usados e estudados em teoria estrutural da demonstração. A dedução natural manipula fórmulas, procura modelar o raciocínio informal usado, por exemplo, nas demonstrações matemáticas, e tem relações priveligiadas com o lambda-calculus e, por via deste, com a programação funcional. O cálculo de sequentes manipula instâncias formais da relação de consequência lógica, procura modelar uma dualidade entre hipótese e conclusão, e é especialmente adequado para a busca semi-automática de demonstrações, tendo, por isso, relações priveligiadas com a programação em lógica. A investigação das últimas décadas mostrou que estas e outras diferenças são mais aparentes do que reais. Neste seminário vamos ilustrar alguns resultados recentes e, de algum modo radicais, neste processo de "unificação", que se obtêm a partir do momento em que se compreende a relação do cálculo de sequentes com o lambda-calculus, e desde que se esteja preparado para aceitar um alargamento do conceito de dedução natural.